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);