22 #ifndef _cvc3__include__vcl_h_
23 #define _cvc3__include__vcl_h_
44 class TheoryBitvector;
97 : d_idx(idx), d_thm(thm), d_tcc(tcc) { }
143 void getAssumptionsRec(
const Theorem& thm,
144 std::set<UserAssertion>& assumptions,
148 void getAssumptions(
const Assumptions& a, std::vector<Expr>& assumptions);
153 #ifdef _CVC3_DEBUG_MODE
155 void dumpTrace(
int scope);
171 void reprocessFlags();
179 Type subtypeType(
const Expr& pred,
const Expr& witness);
182 Type tupleType(
const std::vector<Type>& types);
183 Type recordType(
const std::string& field,
const Type& type);
184 Type recordType(
const std::string& field0,
const Type& type0,
185 const std::string& field1,
const Type& type1);
186 Type recordType(
const std::string& field0,
const Type& type0,
187 const std::string& field1,
const Type& type1,
188 const std::string& field2,
const Type& type2);
189 Type recordType(
const std::vector<std::string>& fields,
190 const std::vector<Type>& types);
191 Type dataType(
const std::string& name,
192 const std::string& constructor,
193 const std::vector<std::string>& selectors,
194 const std::vector<Expr>& types);
195 Type dataType(
const std::string& name,
196 const std::vector<std::string>& constructors,
197 const std::vector<std::vector<std::string> >& selectors,
198 const std::vector<std::vector<Expr> >& types);
199 void dataType(
const std::vector<std::string>& names,
200 const std::vector<std::vector<std::string> >& constructors,
201 const std::vector<std::vector<std::vector<std::string> > >& selectors,
202 const std::vector<std::vector<std::vector<Expr> > >& types,
203 std::vector<Type>& returnTypes);
205 Type bitvecType(
int n);
207 Type funType(
const std::vector<Type>& typeDom,
const Type& typeRan);
208 Type createType(
const std::string& typeName);
209 Type createType(
const std::string& typeName,
const Type& def);
210 Type lookupType(
const std::string& typeName);
213 Expr varExpr(
const std::string& name,
const Type& type);
214 Expr varExpr(
const std::string& name,
const Type& type,
const Expr& def);
215 Expr lookupVar(
const std::string& name,
Type* type);
220 Expr stringExpr(
const std::string& str);
221 Expr idExpr(
const std::string& name);
222 Expr listExpr(
const std::vector<Expr>& kids);
226 Expr listExpr(
const std::string& op,
const std::vector<Expr>& kids);
227 Expr listExpr(
const std::string& op,
const Expr& e1);
228 Expr listExpr(
const std::string& op,
const Expr& e1,
230 Expr listExpr(
const std::string& op,
const Expr& e1,
232 void printExpr(
const Expr& e);
233 void printExpr(
const Expr& e, std::ostream& os);
238 void cmdsFromString(
const std::string& s,
InputLanguage lang);
239 Expr exprFromString(
const std::string& s);
247 Expr orExpr(
const std::vector<Expr>& children);
251 Expr distinctExpr(
const std::vector<Expr>& children);
252 Expr iteExpr(
const Expr& ifpart,
const Expr& thenpart,
const Expr& elsepart);
254 Op createOp(
const std::string& name,
const Type& type);
255 Op createOp(
const std::string& name,
const Type& type,
const Expr& def);
256 Op lookupOp(
const std::string& name,
Type* type);
257 Expr funExpr(
const Op& op,
const Expr& child);
259 Expr funExpr(
const Op& op,
const Expr& child0,
const Expr& child1,
const Expr& child2);
260 Expr funExpr(
const Op& op,
const std::vector<Expr>& children);
262 bool addPairToArithOrder(
const Expr& smaller,
const Expr& bigger);
263 Expr ratExpr(
int n,
int d);
264 Expr ratExpr(
const std::string& n,
const std::string& d,
int base);
265 Expr ratExpr(
const std::string& n,
int base);
278 Expr recordExpr(
const std::string& field,
const Expr& expr);
279 Expr recordExpr(
const std::string& field0,
const Expr& expr0,
280 const std::string& field1,
const Expr& expr1);
281 Expr recordExpr(
const std::string& field0,
const Expr& expr0,
282 const std::string& field1,
const Expr& expr1,
283 const std::string& field2,
const Expr& expr2);
284 Expr recordExpr(
const std::vector<std::string>& fields,
285 const std::vector<Expr>& exprs);
286 Expr recSelectExpr(
const Expr& record,
const std::string& field);
287 Expr recUpdateExpr(
const Expr& record,
const std::string& field,
288 const Expr& newValue);
293 Expr newBVConstExpr(
const std::string& s,
int base);
294 Expr newBVConstExpr(
const std::vector<bool>& bits);
297 Expr newConcatExpr(
const std::vector<Expr>& kids);
298 Expr newBVExtractExpr(
const Expr& e,
int hi,
int low);
301 Expr newBVAndExpr(
const std::vector<Expr>& kids);
303 Expr newBVOrExpr(
const std::vector<Expr>& kids);
305 Expr newBVXorExpr(
const std::vector<Expr>& kids);
307 Expr newBVXnorExpr(
const std::vector<Expr>& kids);
315 Expr newSXExpr(
const Expr& t1,
int len);
316 Expr newBVUminusExpr(
const Expr& t1);
318 Expr newBVPlusExpr(
int numbits,
const std::vector<Expr>& k);
319 Expr newBVPlusExpr(
int numbits,
const Expr& t1,
const Expr& t2);
320 Expr newBVMultExpr(
int numbits,
const Expr& t1,
const Expr& t2);
326 Expr newFixedLeftShiftExpr(
const Expr& t1,
int r);
327 Expr newFixedConstWidthLeftShiftExpr(
const Expr& t1,
int r);
328 Expr newFixedRightShiftExpr(
const Expr& t1,
int r);
334 Expr tupleExpr(
const std::vector<Expr>& exprs);
335 Expr tupleSelectExpr(
const Expr& tuple,
int index);
336 Expr tupleUpdateExpr(
const Expr& tuple,
int index,
const Expr& newValue);
337 Expr datatypeConsExpr(
const std::string& constructor,
338 const std::vector<Expr>& args);
339 Expr datatypeSelExpr(
const std::string& selector,
const Expr& arg);
340 Expr datatypeTestExpr(
const std::string& constructor,
const Expr& arg);
341 Expr boundVarExpr(
const std::string& name,
const std::string& uid,
343 Expr forallExpr(
const std::vector<Expr>& vars,
const Expr& body);
344 Expr forallExpr(
const std::vector<Expr>& vars,
const Expr& body,
const Expr& trigger);
345 Expr forallExpr(
const std::vector<Expr>& vars,
const Expr& body,
346 const std::vector<Expr>& triggers);
347 Expr forallExpr(
const std::vector<Expr>& vars,
const Expr& body,
348 const std::vector<std::vector<Expr> >& triggers);
350 void setTriggers(
const Expr& e,
const std::vector<std::vector<Expr> >& triggers);
351 void setTriggers(
const Expr& e,
const std::vector<Expr>& triggers);
352 void setTrigger(
const Expr& e,
const Expr& trigger);
353 void setMultiTrigger(
const Expr& e,
const std::vector<Expr>& multiTrigger);
355 Expr existsExpr(
const std::vector<Expr>& vars,
const Expr& body);
356 Op lambdaExpr(
const std::vector<Expr>& vars,
const Expr& body);
357 Op transClosure(
const Op& op);
359 const std::vector<Expr>& inputs,
const Expr& n);
361 void setResourceLimit(
unsigned limit);
362 void setTimeLimit(
unsigned limit);
363 void assertFormula(
const Expr& e);
364 void registerAtom(
const Expr& e);
365 Expr getImpliedLiteral();
372 void returnFromCheck();
373 void getUserAssumptions(std::vector<Expr>& assumptions);
374 void getInternalAssumptions(std::vector<Expr>& assumptions);
375 void getAssumptions(std::vector<Expr>& assumptions);
376 void getAssumptionsUsed(std::vector<Expr>& assumptions);
377 Expr getProofQuery();
378 void getCounterExample(std::vector<Expr>& assumptions,
bool inOrder);
382 bool inconsistent(std::vector<Expr>& assumptions);
385 bool incomplete(std::vector<std::string>& reasons);
387 Expr getAssignment();
390 void getAssumptionsTCC(std::vector<Expr>& assumptions);
393 Proof getProofClosure();
398 void popto(
int stackLevel);
402 void poptoScope(
int scopeLevel);
405 void logAnnotation(
const Expr& annot);
407 void loadFile(
const std::string& fileName,
409 bool interactive =
false,
410 bool calledFromParser =
false);
411 void loadFile(std::istream& is,
413 bool interactive =
false);
417 unsigned long getMemory(
int verbosity = 0);
Expr minusExpr(const Expr &left, const Expr &right)
ExprStream & pop(ExprStream &os)
Restore the indentation.
CLFlags * d_flags
Command line flags.
API to to a generic proof search engine.
Expr ltExpr(const Expr &left, const Expr &right)
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
ExprStream & reset(ExprStream &os)
Reset the indentation to the default at this level.
Generic API for a validity checker.
This theory handles basic linear arithmetic.
Theorem3 d_lastQuery
Result of the last query()
Type arrayType(const Type &type1, const Type &type2)
InputLanguage
Different input languages.
MS C++ specific settings.
"Theory" of symbolic simulation.
This theory handles uninterpreted functions.
Theorem d_lastQueryTCC
Result of the last query(e, true) (for a TCC).
Statistics * d_statistics
Run-time statistics.
TheoryRecords * d_theoryRecords
Expr gtExpr(const Expr &left, const Expr &right)
TheoryBitvector * d_theoryBitvector
CDO< int > * d_stackLevel
User-level view of the scope stack.
CDMap< Expr, UserAssertion > * d_userAssertions
Backtracking map of user assertions.
CLFlags & getFlags() const
Return the set of command-line flags.
Description: Counters and flags for collecting run-time statistics.
ExprManager * d_em
Pointers to main system components.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
const Theorem & thm() const
Fetching a Theorem.
Expr orExpr(const std::vector< Expr > &children)
bool d_modelStackPushed
True iff we've pushed the stack artificially to avoid polluting context.
CDO< unsigned > * d_batchedAssertionsIdx
Index into batched Assertions.
TheoryQuant * d_theoryQuant
TheoryArith * d_theoryArith
bool d_dump
Whether to dump a trace (or a translated version)
void printStatistics()
Print collected statistics to stdout.
const Theorem & tcc() const
Fetching a TCC.
This theory handles datatypes.
Translator * d_translator
ExprManager * getEM()
Return the ExprManager.
Expr powExpr(const Expr &pow, const Expr &base)
Power (x^n, or base^{pow}) expressions.
Generic API for a validity checker.
This theory handles records.
std::vector< Theory * > d_theories
All theories are stored in this common vector.
UserAssertion()
The proof of its TCC.
TheorySimulate * d_theorySimulate
This theory handles arrays.
Expr plusExpr(const Expr &left, const Expr &right)
Expr geExpr(const Expr &left, const Expr &right)
size_t d_nextIdx
Next index for user assertion.
Theorem3 d_lastClosure
Closure of the last query(e): |- Gamma => e.
TheoryArray * d_theoryArray
Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)
Manager for multiple contexts. Also holds current context.
UserAssertion(const Theorem &thm, const Theorem &tcc, size_t idx)
Constructor.
TheoryCore * d_theoryCore
Pointers to theories.
Expr uminusExpr(const Expr &child)
TheoryDatatype * d_theoryDatatype
Expr leExpr(const Expr &left, const Expr &right)
CDList< Expr > * d_batchedAssertions
Backtracking map of assertions when assertion batching is on.
Structure to hold user assertions indexed by declaration order.
Expr divideExpr(const Expr &left, const Expr &right)
Expr andExpr(const std::vector< Expr > &children)
This theory handles quantifiers.
Expr multExpr(const Expr &left, const Expr &right)
Theorem d_tcc
The theorem of the assertion (a |- a)
friend bool operator<(const UserAssertion &a1, const UserAssertion &a2)
Comparison for use in std::map, to sort in declaration order.
Nice SAL-like language for manually written specs.
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
Statistics & getStatistics()
Get statistics object.