cvc4-1.3
c_interface.h
Go to the documentation of this file.
1 /*****************************************************************************/
20 /*****************************************************************************/
21 
22 #include "cvc4_public.h"
23 
24 #ifndef _cvc3__include__c_interface_h_
25 #define _cvc3__include__c_interface_h_
26 
28 
34 
37 void vc_deleteFlags(Flags flags);
39 void vc_deleteType(Type t);
41 void vc_deleteExpr(Expr e);
43 void vc_deleteOp(Op op);
45 void vc_deleteVector(Expr* e);
47 void vc_deleteTypeVector(Type* e);
48 
49 // Setting the flags
51 void vc_setBoolFlag(Flags flags, char* name, int val);
53 void vc_setIntFlag(Flags flags, char* name, int val);
55 void vc_setStringFlag(Flags flags, char* name, char* val);
57 void vc_setStrSeqFlag(Flags flags, char* name, char* str, int val);
58 
59 // Basic types
60 Type vc_boolType(VC vc);
61 Type vc_realType(VC vc);
62 Type vc_intType(VC vc);
63 
65 Type vc_subRangeType(VC vc, int lowerEnd, int upperEnd);
66 
68 
79 Type vc_subtypeType(VC vc, Expr pred, Expr witness);
80 
81 // Tuple types
82 Type vc_tupleType2(VC vc, Type type0, Type type1);
83 Type vc_tupleType3(VC vc, Type type0, Type type1, Type type2);
85 Type vc_tupleTypeN(VC vc, Type* types, int numTypes);
86 
87 // Record types
88 Type vc_recordType1(VC vc, char* field, Type type);
89 Type vc_recordType2(VC vc, char* field0, Type type0,
90  char* field1, Type type1);
91 Type vc_recordType3(VC vc, char* field0, Type type0,
92  char* field1, Type type1,
93  char* field2, Type type2);
95 
96 Type vc_recordTypeN(VC vc, char** fields, Type* types, int numFields);
97 
98 // Datatypes
99 
101 
104 Type vc_dataType1(VC vc, char* name, char* constructor, int arity,
105  char** selectors, Expr* types);
106 
108 
111 Type vc_dataTypeN(VC vc, char* name, int numCons, char** constructors,
112  int* arities, char*** selectors, Expr** types);
113 
115 
121 Type* vc_dataTypeMN(VC vc, int numTypes, char** names,
122  int* numCons, char*** constructors,
123  int** arities, char**** selectors,
124  Expr*** types);
125 
127 Type vc_arrayType(VC vc, Type typeIndex, Type typeData);
128 
130 Type vc_bvType(VC vc, int n);
131 
133 Type vc_funType1(VC vc, Type a1, Type typeRan);
135 Type vc_funType2(VC vc, Type a1, Type a2, Type typeRan);
137 Type vc_funType3(VC vc, Type a1, Type a2, Type a3, Type typeRan);
139 Type vc_funTypeN(VC vc, Type* args, Type typeRan, int numArgs);
140 
141 // User-defined types
142 
144 Type vc_createType(VC vc, char* typeName);
146 Type vc_lookupType(VC vc, char* typeName);
147 
149 // Expr manipulation methods //
151 
153 ExprManager* vc_getEM(VC vc);
154 
156 
157 Expr vc_varExpr(VC vc, char* name, Type type);
158 
160 Expr vc_varExprDef(VC vc, char* name, Type type,
161  Expr def);
162 
164 
165 Expr vc_lookupVar(VC vc, char* name, Type* type);
166 
168 Type vc_getType(VC vc, Expr e);
169 
171 Type vc_getBaseType(VC vc, Expr e);
172 
175 
177 Expr vc_getTypePred(VC vc, Type t, Expr e);
178 
180 Expr vc_stringExpr(VC vc, char* str);
181 
183 Expr vc_idExpr(VC vc, char* name);
184 
186 
206 Expr vc_listExpr(VC vc, int numKids, Expr* kids);
207 
208 // Expr I/O
210 void vc_printExpr(VC vc, Expr e);
212 
215 char* vc_printExprString(VC vc, Expr e);
217 void vc_deleteString(char* str);
219 void vc_printExprFile(VC vc, Expr e, int fd);
220 
222 
231 Expr vc_importExpr(VC vc, Expr e);
232 
234 
236 
238 Expr vc_eqExpr(VC vc, Expr child0, Expr child1);
239 
241 Expr vc_distinctExpr(VC vc, Expr* children, int numChildren);
242 
243 // Boolean expressions
244 
245 // The following functions create Boolean expressions. The children provided
246 // as arguments must be of type Boolean.
247 Expr vc_trueExpr(VC vc);
248 Expr vc_falseExpr(VC vc);
249 Expr vc_notExpr(VC vc, Expr child);
250 Expr vc_andExpr(VC vc, Expr left, Expr right);
251 Expr vc_andExprN(VC vc, Expr* children, int numChildren);
252 Expr vc_orExpr(VC vc, Expr left, Expr right);
253 Expr vc_orExprN(VC vc, Expr* children, int numChildren);
254 Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc);
255 Expr vc_iffExpr(VC vc, Expr left, Expr right);
256 Expr vc_iteExpr(VC vc, Expr ifpart, Expr thenpart, Expr elsepart);
257 
258 // Substitution
259 
260 // Substitutes oldTerms for newTerms in e.
261 // This function doesn't actually exist in ValidityChecker interface,
262 // but it does in Expr, and its functionality is needed in the C interface.
263 // For consistency, it is represented here as if it were in ValidityChecker.
264 Expr vc_substExpr(VC vc, Expr e,
265  Expr* oldTerms, int numOldTerms,
266  Expr* newTerms, int numNewTerms);
267 
268 // User-defined (uninterpreted) functions.
269 
271 
272 Op vc_createOp(VC vc, char* name, Type type);
273 
275 Op vc_createOpDef(VC vc, char* name, Type type, Expr def);
276 
278 
281 Op vc_lookupOp(VC vc, char* name, Type* type);
282 
284 
285 Expr vc_funExpr1(VC vc, Op op, Expr child);
286 Expr vc_funExpr2(VC vc, Op op, Expr left, Expr right);
287 Expr vc_funExpr3(VC vc, Op op, Expr child0, Expr child1, Expr child2);
288 Expr vc_funExprN(VC vc, Op op, Expr* children, int numChildren);
289 
290 // Arithmetic
291 
293 
294 Expr vc_ratExpr(VC vc, int n, int d);
295 
297 
299 Expr vc_ratExprFromStr(VC vc, char* n, char* d, int base);
300 
302 
308 Expr vc_ratExprFromStr1(VC vc, char* n, int base);
309 
311 Expr vc_uminusExpr(VC vc, Expr child);
312 
313 // plus, minus, mult. Children must have numeric types.
314 Expr vc_plusExpr(VC vc, Expr left, Expr right);
315 Expr vc_plusExprN(VC vc, Expr* children, int numChildren);
316 Expr vc_minusExpr(VC vc, Expr left, Expr right);
317 Expr vc_multExpr(VC vc, Expr left, Expr right);
318 Expr vc_powExpr(VC vc, Expr pow, Expr base);
319 Expr vc_divideExpr(VC vc, Expr numerator, Expr denominator);
320 
321 // The following functions create less-than, less-than or equal,
322 // greater-than, and greater-than or equal expressions of type Boolean.
323 // Their arguments must be of numeric types.
324 Expr vc_ltExpr(VC vc, Expr left, Expr right);
325 Expr vc_leExpr(VC vc, Expr left, Expr right);
326 Expr vc_gtExpr(VC vc, Expr left, Expr right);
327 Expr vc_geExpr(VC vc, Expr left, Expr right);
328 
329 // Records
330 
331 // Create record literals;
332 Expr vc_recordExpr1(VC vc, char* field, Expr expr);
333 Expr vc_recordExpr2(VC vc, char* field0, Expr expr0,
334  char* field1, Expr expr1);
335 Expr vc_recordExpr3(VC vc, char* field0, Expr expr0,
336  char* field1, Expr expr1,
337  char* field2, Expr expr2);
338 Expr vc_recordExprN(VC vc, char** fields, Expr* exprs, int numFields);
339 
341 Expr vc_recSelectExpr(VC vc, Expr record, char* field);
342 
344 Expr vc_recUpdateExpr(VC vc, Expr record, char* field, Expr newValue);
345 
346 // Arrays
347 
349 Expr vc_readExpr(VC vc, Expr array, Expr index);
350 
352 Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue);
353 
354 // Bitvectors
355 // Additional type constructor
356 Type vc_bv32Type(VC vc);
357 
358 // Bitvector constants
359 Expr vc_bvConstExprFromStr(VC vc, char* binary_repr);
360 Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value);
361 Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value);
362 Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long value);
363 
364 // Concat and extract
365 Expr vc_bvConcatExpr(VC vc, Expr left, Expr right);
366 Expr vc_bvConcatExprN(VC vc, Expr* children, int numChildren);
367 Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no);
368 Expr vc_bvBoolExtract(VC vc, Expr child, int bit_no);
369 
370 // Bitwise Boolean operators: Negation, And, Or, Xor
371 Expr vc_bvNotExpr(VC vc, Expr child);
372 Expr vc_bvAndExpr(VC vc, Expr left, Expr right);
373 Expr vc_bvOrExpr(VC vc, Expr left, Expr right);
374 Expr vc_bvXorExpr(VC vc, Expr left, Expr right);
375 
376 // Unsigned bitvector inequalities
377 Expr vc_bvLtExpr(VC vc, Expr left, Expr right);
378 Expr vc_bvLeExpr(VC vc, Expr left, Expr right);
379 Expr vc_bvGtExpr(VC vc, Expr left, Expr right);
380 Expr vc_bvGeExpr(VC vc, Expr left, Expr right);
381 
382 // Signed bitvector inequalities
383 Expr vc_bvSLtExpr(VC vc, Expr left, Expr right);
384 Expr vc_bvSLeExpr(VC vc, Expr left, Expr right);
385 Expr vc_bvSGtExpr(VC vc, Expr left, Expr right);
386 Expr vc_bvSGeExpr(VC vc, Expr left, Expr right);
387 
388 // Sign-extend child to a total of nbits bits
389 Expr vc_bvSignExtend(VC vc, Expr child, int nbits);
390 
391 // Bitvector arithmetic: unary minus, plus, subtract, multiply
392 Expr vc_bvUMinusExpr(VC vc, Expr child);
393 Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right);
394 Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right);
395 Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right);
396 Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right);
397 Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right);
398 Expr vc_bv32MultExpr(VC vc, Expr left, Expr right);
399 Expr vc_bvUDivExpr(VC vc, Expr left, Expr right);
400 Expr vc_bvURemExpr(VC vc, Expr left, Expr right);
401 Expr vc_bvSDivExpr(VC vc, Expr left, Expr right);
402 Expr vc_bvSRemExpr(VC vc, Expr left, Expr right);
403 Expr vc_bvSModExpr(VC vc, Expr left, Expr right);
404 
405 // Shift operators
406 Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child);
407 Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child);
408 Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child);
409 Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child);
410 Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child);
411 Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child);
413 
414 /*C pointer support: C interface to support C memory arrays in CVC3 */
415 Expr vc_bvCreateMemoryArray(VC vc, char * arrayName);
417  Expr array, Expr byteIndex, int numOfBytes);
419  Expr array, Expr byteIndex,
420  Expr element, int numOfBytes);
421 
422 // Tuples
423 
425 
426 Expr vc_tupleExprN(VC vc, Expr* children, int numChildren);
427 
429 Expr vc_tupleSelectExpr(VC vc, Expr tuple, int index);
430 
432 Expr vc_tupleUpdateExpr(VC vc, Expr tuple, int index, Expr newValue);
433 
434 // Datatypes
435 
437 Expr vc_datatypeConsExpr(VC vc, char* constructor, int numArgs, Expr* args);
438 
440 Expr vc_datatypeSelExpr(VC vc, char* selector, Expr arg);
441 
443 Expr vc_datatypeTestExpr(VC vc, char* constructor, Expr arg);
444 
445 // Quantifiers
446 
448 
454 Expr vc_boundVarExpr(VC vc, char* name, char *uid, Type type);
455 
457 
458 Type vc_forallExpr(VC vc, Expr* Bvars, int numBvars, Expr f);
459 
461 void vc_setTriggers(VC vc, Expr e, int numTrigs, Expr* triggers);
462 
464 
465 Expr vc_existsExpr(VC vc, Expr* Bvars, int numBvars, Expr f);
466 
468 Op vc_lambdaExpr(VC vc, int numVars, Expr* vars, Expr body);
469 
471 // Context-related methods //
473 
475 
476 void vc_setResourceLimit(VC vc, unsigned limit);
477 
479 
480 void vc_assertFormula(VC vc, Expr e);
481 
483 
486 void vc_registerAtom(VC vc, Expr e);
487 
489 
492 
494 Expr vc_simplify(VC vc, Expr e);
495 
497 
505 int vc_query(VC vc, Expr e);
506 
508 
510 int vc_checkContinue(VC vc);
511 
513 
515 int vc_restart(VC vc, Expr e);
516 
518 
520 void vc_returnFromCheck(VC vc);
521 
523 
528 Expr* vc_getUserAssumptions(VC vc, int* size);
529 
531 
535 Expr* vc_getInternalAssumptions(VC vc, int* size);
536 
538 
542 Expr* vc_getAssumptions(VC vc, int* size);
543 
544 //yeting, for proof translation, get the assumptions used.
545 //the assumptions used are different from the user assumptions.
546 //the assumptions used are preprocessed if 'preprocess' is ena
548 
549 //yeting, for proof translation,
551 
553 
558 Expr* vc_getAssumptionsUsed(VC vc, int* size);
559 
561 
567 Expr* vc_getCounterExample(VC vc, int* size);
568 
570 
575 Expr* vc_getConcreteModel(VC vc, int* size);
576 
577 // Returns true if the current context is inconsistent.
582 int vc_inconsistent(VC vc, Expr** assumptions, int* size);
583 
585 
590 char* vc_incomplete(VC vc);
591 
593 Expr vc_getProof(VC vc);
594 
596 Expr vc_getProofOfFile(VC vc, char * filename);
597 
599 
600 Expr vc_getTCC(VC vc);
601 
603 
606 Expr* vc_getAssumptionsTCC(VC vc, int* size);
607 
609 
611 
613 
618 Expr vc_getClosure(VC vc);
619 
621 
623 
625 int vc_stackLevel(VC vc);
626 
628 void vc_push(VC vc);
629 
631 void vc_pop(VC vc);
632 
634 
636 void vc_popto(VC vc, int stackLevel);
637 
640 
641 /* ---------------------------------------------------------------------- */
642 /* Util */
643 /* ---------------------------------------------------------------------- */
644 
645 // Order
646 
648 
653 int vc_compare_exprs(Expr e1,Expr e2);
654 
655 // Printing
656 
658 char* vc_exprString(Expr e);
660 char* vc_typeString(Type t);
661 
662 // What kind of Expr?
663 int vc_isClosure(Expr e);
664 int vc_isQuantifier(Expr e);
665 int vc_isLambda(Expr e);
666 Expr vc_isVar(Expr e);
667 
668 int vc_arity(Expr e);
669 int vc_getKind(Expr e);
670 Expr vc_getChild(Expr e, int i);
671 int vc_getNumVars(Expr e);
672 Expr vc_getVar(Expr e, int i);
673 Expr vc_getBody(Expr e);
675 Expr vc_getFun(VC vc, Expr e);
676 Expr vc_toExpr(Type t);
677 
679 const char* vc_getKindString(VC vc,int kind);
680 
682 int vc_getKindInt(VC vc,char* kind_name);
683 
685 int vc_getInt(Expr e);
686 
688 int vc_getBVInt(VC vc, Expr e);
690 unsigned int vc_getBVUnsigned(VC vc, Expr e);
691 
692 // Debug
693 int vc_get_error_status();
694 void vc_reset_error_status();
695 char* vc_get_error_string();
696 
698 void vc_print_statistics(VC vc);
699 
700 #endif
701 
702 
Expr vc_simplify(VC vc, Expr e)
Simplify e with respect to the current context.
Expr vc_trueExpr(VC vc)
Expr vc_tupleExprN(VC vc, Expr *children, int numChildren)
Create a tuple expression.
Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right)
Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right)
Expr vc_importExpr(VC vc, Expr e)
Import the Expr from another instance of VC.
Expr vc_getChild(Expr e, int i)
void * Flags
Type vc_dataType1(VC vc, char *name, char *constructor, int arity, char **selectors, Expr *types)
Single datatype, single constructor.
char * vc_exprString(Expr e)
Convert Expr to string.
void * Expr
void vc_deleteExpr(Expr e)
Delete expression.
Type vc_getBaseTypeOfType(VC vc, Type t)
Get the largest supertype of the Type.
Type vc_boolType(VC vc)
Expr vc_bvConcatExpr(VC vc, Expr left, Expr right)
Op vc_createOpDef(VC vc, char *name, Type type, Expr def)
Create a named user-defined function with a given type.
Expr vc_bvReadMemoryArray(VC vc, Expr array, Expr byteIndex, int numOfBytes)
Expr vc_getClosure(VC vc)
After successful query, return its closure |- Gamma => phi.
void * VC
Expr vc_orExprN(VC vc, Expr *children, int numChildren)
void vc_returnFromCheck(VC vc)
Returns to context immediately before last invalid query.
Expr vc_ratExprFromStr(VC vc, char *n, char *d, int base)
Create a rational number n/d; n and d are given as strings.
void vc_pop(VC vc)
Restore the current context to its state at the last checkpoint.
Expr vc_bvSLtExpr(VC vc, Expr left, Expr right)
int vc_getKindInt(VC vc, char *kind_name)
Translate a kind string to an int.
Type vc_funTypeN(VC vc, Type *args, Type typeRan, int numArgs)
Create a function type with N arguments.
void vc_setStringFlag(Flags flags, char *name, char *val)
Set a string flag to the given value.
Expr vc_bvSDivExpr(VC vc, Expr left, Expr right)
Flags vc_createFlags()
Create validity checker's flags.
void * ExprManager
Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, int low_bit_no)
Expr vc_getProof(VC vc)
Returns the proof for the last proven query.
Expr vc_bvSGtExpr(VC vc, Expr left, Expr right)
Expr vc_getProofClosure(VC vc)
Construct a proof of the query closure |- Gamma => phi.
Expr vc_bvConcatExprN(VC vc, Expr *children, int numChildren)
void vc_deleteVector(Expr *e)
Delete vector of expressions.
Type vc_createType(VC vc, char *typeName)
Create an uninterpreted named type.
void vc_destroyValidityChecker(VC vc)
Destroy the validity checker.
void vc_printExpr(VC vc, Expr e)
Expr vc_parseExpr(VC vc, char* s);.
Expr vc_bvLeExpr(VC vc, Expr left, Expr right)
Expr vc_ratExpr(VC vc, int n, int d)
Create a rational number with numerator n and denominator d.
void vc_popto(VC vc, int stackLevel)
Restore the current context to the given stackLevel.
Expr vc_datatypeConsExpr(VC vc, char *constructor, int numArgs, Expr *args)
Datatype constructor expression.
Expr vc_recSelectExpr(VC vc, Expr record, char *field)
Create an expression representing the selection of a field from a record.
Type vc_realType(VC vc)
char * vc_printExprString(VC vc, Expr e)
Print e into a char*.
Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc)
void vc_setTriggers(VC vc, Expr e, int numTrigs, Expr *triggers)
Set triggers for a forallExpr.
Expr vc_bvAndExpr(VC vc, Expr left, Expr right)
int vc_query(VC vc, Expr e)
Check validity of e in the current context.
Expr vc_varExprDef(VC vc, char *name, Type type, Expr def)
Create a variable with a given name, type, and value.
void vc_deleteFlags(Flags flags)
Delete the flags.
Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right)
unsigned int vc_getBVUnsigned(VC vc, Expr e)
Return an unsigned int from a constant bitvector expression.
Expr * vc_getInternalAssumptions(VC vc, int *size)
Get assumptions made internally in this and all previous contexts.
Expr vc_bvNotExpr(VC vc, Expr child)
Type vc_subtypeType(VC vc, Expr pred, Expr witness)
Creates a subtype defined by the given predicate.
Expr vc_funExpr3(VC vc, Op op, Expr child0, Expr child1, Expr child2)
Expr vc_funExprN(VC vc, Op op, Expr *children, int numChildren)
Expr vc_plusExprN(VC vc, Expr *children, int numChildren)
void vc_reset_error_status()
Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value)
Expr * vc_getAssumptions(VC vc, int *size)
Get all assumptions made in this and all previous contexts.
int vc_getNumVars(Expr e)
int vc_getBVInt(VC vc, Expr e)
Return an int from a constant bitvector expression.
Type vc_forallExpr(VC vc, Expr *Bvars, int numBvars, Expr f)
Create a FORALL quantifier.
Op vc_lambdaExpr(VC vc, int numVars, Expr *vars, Expr body)
Lambda-expression.
const char * vc_getKindString(VC vc, int kind)
Translate a kind int to a string.
Type vc_bvType(VC vc, int n)
Create a bitvector type of length n.
Expr vc_plusExpr(VC vc, Expr left, Expr right)
Type vc_recordType3(VC vc, char *field0, Type type0, char *field1, Type type1, char *field2, Type type2)
Expr vc_gtExpr(VC vc, Expr left, Expr right)
Expr vc_isVar(Expr e)
Expr vc_existsExpr(VC vc, Expr *Bvars, int numBvars, Expr f)
Create an EXISTS quantifier.
Type vc_subRangeType(VC vc, int lowerEnd, int upperEnd)
Create a subrange type.
int vc_isQuantifier(Expr e)
Expr vc_notExpr(VC vc, Expr child)
Expr vc_funExpr1(VC vc, Op op, Expr child)
Create expressions with a user-defined operator.
Expr vc_getTCC(VC vc)
Returns the TCC of the last assumption or query.
Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child)
Op vc_lookupOp(VC vc, char *name, Type *type)
Lookup an operator by name.
Type vc_funType3(VC vc, Type a1, Type a2, Type a3, Type typeRan)
Create a function type with 3 arguments.
VC vc_createValidityChecker(Flags flags)
Flags can be NULL.
Expr vc_getProofTCC(VC vc)
Returns the proof of TCC of the last assumption or query.
Expr vc_ltExpr(VC vc, Expr left, Expr right)
void vc_printExprFile(VC vc, Expr e, int fd)
Print 'e' into an open file descriptor.
Expr vc_getFun(VC vc, Expr e)
Expr vc_geExpr(VC vc, Expr left, Expr right)
Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right)
Expr vc_datatypeTestExpr(VC vc, char *constructor, Expr arg)
Datatype tester expression.
ExprManager * vc_getEM(VC vc)
Return the ExprManager.
Expr vc_bv32MultExpr(VC vc, Expr left, Expr right)
Type vc_tupleTypeN(VC vc, Type *types, int numTypes)
Create a tuple type. 'types' is an array of types of length numTypes.
void vc_setStrSeqFlag(Flags flags, char *name, char *str, int val)
Add a (string, bool) pair to the multy-string flag.
int vc_inconsistent(VC vc, Expr **assumptions, int *size)
Expr vc_bvGeExpr(VC vc, Expr left, Expr right)
Expr vc_getVar(Expr e, int i)
Expr vc_tupleSelectExpr(VC vc, Expr tuple, int index)
Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)
Expr vc_substExpr(VC vc, Expr e, Expr *oldTerms, int numOldTerms, Expr *newTerms, int numNewTerms)
Type vc_recordTypeN(VC vc, char **fields, Type *types, int numFields)
Create a record type.
Expr vc_bvConstExprFromStr(VC vc, char *binary_repr)
Expr vc_lookupVar(VC vc, char *name, Type *type)
Get the expression and type associated with a name.
Expr vc_powExpr(VC vc, Expr pow, Expr base)
Expr vc_multExpr(VC vc, Expr left, Expr right)
void vc_deleteOp(Op op)
Delete operator.
Expr * vc_getAssumptionsUsed(VC vc, int *size)
Returns the set of assumptions used in the proof of queried formula.
Expr vc_readExpr(VC vc, Expr array, Expr index)
Create an expression for the value of array at the given index.
Expr vc_bvSignExtend(VC vc, Expr child, int nbits)
Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child)
Expr vc_bvUMinusExpr(VC vc, Expr child)
Expr vc_uminusExpr(VC vc, Expr child)
Unary minus. Child must have a numeric type.
Expr vc_bvSLeExpr(VC vc, Expr left, Expr right)
Type * vc_dataTypeMN(VC vc, int numTypes, char **names, int *numCons, char ***constructors, int **arities, char ****selectors, Expr ***types)
Multiple datatypes.
Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child)
int vc_getInt(Expr e)
Return an int from a rational expression.
Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child)
void vc_print_statistics(VC vc)
Print statistics.
int vc_stackLevel(VC vc)
Returns the current stack level. Initial level is 0.
Expr * vc_getConcreteModel(VC vc, int *size)
Will assign concrete values to all user created variables.
Expr vc_funExpr2(VC vc, Op op, Expr left, Expr right)
Expr * vc_getAssumptionsTCC(VC vc, int *size)
Return the set of assumptions used in the proof of the last TCC.
void vc_deleteTypeVector(Type *e)
Delete vector of types.
int vc_arity(Expr e)
Expr vc_ratExprFromStr1(VC vc, char *n, int base)
Create a rational from a single string.
Expr vc_bvSGeExpr(VC vc, Expr left, Expr right)
void vc_deleteType(Type t)
Delete type.
Macros that should be defined everywhere during the building of the libraries and driver binary...
Expr vc_eqExpr(VC vc, Expr child0, Expr child1)
Create an equality expression. The two children must have the same type.
void vc_setIntFlag(Flags flags, char *name, int val)
Set an integer flag to the given value.
Type vc_bv32Type(VC vc)
Expr vc_bvSRemExpr(VC vc, Expr left, Expr right)
Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long value)
Type vc_arrayType(VC vc, Type typeIndex, Type typeData)
Create an array type.
Type vc_funType2(VC vc, Type a1, Type a2, Type typeRan)
Create a function type with 2 arguments.
Expr vc_bvCreateMemoryArray(VC vc, char *arrayName)
Expr vc_andExprN(VC vc, Expr *children, int numChildren)
Expr * vc_getCounterExample(VC vc, int *size)
Return the counterexample after a failed query.
Expr vc_toExpr(Type t)
Expr vc_getExistential(Expr e)
Expr vc_bvURemExpr(VC vc, Expr left, Expr right)
Expr vc_getProofOfFile(VC vc, char *filename)
Returns the proof of a .cvc file, if it is valid.
Expr vc_bvWriteToMemoryArray(VC vc, Expr array, Expr byteIndex, Expr element, int numOfBytes)
void * Op
Expr vc_getTypePred(VC vc, Type t, Expr e)
Get the subtype predicate.
Expr vc_getImpliedLiteral(VC vc)
Return next literal implied by last assertion. Null if none.
char * vc_incomplete(VC vc)
Returns non-NULL if the invalid result from last query() is imprecise.
Expr vc_bvSModExpr(VC vc, Expr left, Expr right)
void vc_setBoolFlag(Flags flags, char *name, int val)
Set a boolean flag to true or false.
int vc_compare_exprs(Expr e1, Expr e2)
Compares two expressions.
Expr vc_bvGtExpr(VC vc, Expr left, Expr right)
Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value)
Expr vc_listExpr(VC vc, int numKids, Expr *kids)
Create a list Expr.
Expr vc_getProofQuery(VC vc)
Expr vc_bvUDivExpr(VC vc, Expr left, Expr right)
Expr vc_recordExprN(VC vc, char **fields, Expr *exprs, int numFields)
Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child)
void vc_assertFormula(VC vc, Expr e)
Assert a new formula in the current context.
Expr vc_getProofAssumptions(VC vc)
Expr vc_recUpdateExpr(VC vc, Expr record, char *field, Expr newValue)
Record update; equivalent to "record WITH .field := newValue".
int vc_checkContinue(VC vc)
Get the next model.
Context * vc_getCurrentContext(VC vc)
Get the current context.
Expr vc_recordExpr1(VC vc, char *field, Expr expr)
void vc_registerAtom(VC vc, Expr e)
Register an atomic formula of interest.
int vc_get_error_status()
Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs)
void * Context
Expr vc_getBody(Expr e)
Type vc_getType(VC vc, Expr e)
Get the type of the Expr.
Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child)
Op vc_createOp(VC vc, char *name, Type type)
Create an operator from a function with a given name and type.
Expr vc_iffExpr(VC vc, Expr left, Expr right)
Type vc_tupleType2(VC vc, Type type0, Type type1)
void * Type
Expr vc_recordExpr2(VC vc, char *field0, Expr expr0, char *field1, Expr expr1)
Expr * vc_getUserAssumptions(VC vc, int *size)
Get assumptions made by the user in this and all previous contexts.
Type vc_getBaseType(VC vc, Expr e)
Get the largest supertype of the Expr.
Expr vc_idExpr(VC vc, char *name)
Create an ID Expr.
Expr vc_varExpr(VC vc, char *name, Type type)
Create a variable with a given name and type.
Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right)
Expr vc_distinctExpr(VC vc, Expr *children, int numChildren)
Create an all distinct expression. All children must ahve the same type.
Expr vc_tupleUpdateExpr(VC vc, Expr tuple, int index, Expr newValue)
Tuple update; equivalent to "tuple WITH index := newValue".
Type vc_intType(VC vc)
Type vc_recordType1(VC vc, char *field, Type type)
int vc_isLambda(Expr e)
int vc_restart(VC vc, Expr e)
Restart the most recent query with e as an additional assertion.
Expr vc_bvXorExpr(VC vc, Expr left, Expr right)
Expr vc_bvOrExpr(VC vc, Expr left, Expr right)
int vc_getKind(Expr e)
Expr vc_falseExpr(VC vc)
Expr vc_andExpr(VC vc, Expr left, Expr right)
Type vc_tupleType3(VC vc, Type type0, Type type1, Type type2)
Expr vc_recordExpr3(VC vc, char *field0, Expr expr0, char *field1, Expr expr1, char *field2, Expr expr2)
Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue)
Array update; equivalent to "array WITH [index] := newValue".
Type vc_funType1(VC vc, Type a1, Type typeRan)
Create a function type with 1 argument.
char * vc_typeString(Type t)
Convert Type to string.
char * vc_get_error_string()
Expr vc_divideExpr(VC vc, Expr numerator, Expr denominator)
Expr vc_boundVarExpr(VC vc, char *name, char *uid, Type type)
Create a bound variable.
Type vc_dataTypeN(VC vc, char *name, int numCons, char **constructors, int *arities, char ***selectors, Expr **types)
Single datatype, multiple constructors.
Type vc_importType(Type t)
Import the Type from another instance of VC.
Expr vc_leExpr(VC vc, Expr left, Expr right)
Expr vc_iteExpr(VC vc, Expr ifpart, Expr thenpart, Expr elsepart)
Type vc_lookupType(VC vc, char *typeName)
Lookup a user-defined (uninterpreted) type by name.
Type vc_recordType2(VC vc, char *field0, Type type0, char *field1, Type type1)
Expr vc_minusExpr(VC vc, Expr left, Expr right)
int vc_isClosure(Expr e)
void vc_deleteString(char *str)
Delete char* returned by previous function.
Expr vc_datatypeSelExpr(VC vc, char *selector, Expr arg)
Datatype selector expression.
Expr vc_orExpr(VC vc, Expr left, Expr right)
Expr vc_bvLtExpr(VC vc, Expr left, Expr right)
Expr vc_stringExpr(VC vc, char *str)
Create a string Expr.
void vc_push(VC vc)
Checkpoint the current context and increase the scope level.
void vc_setResourceLimit(VC vc, unsigned limit)
Set the resource limit (0==unlimited, 1==exhausted).
Expr vc_bvBoolExtract(VC vc, Expr child, int bit_no)