CVC3 API (compatibility layer for CVC4) More...

#include <cvc3_compat.h>

Public Member Functions
	ValidityChecker ()
	Constructor. More...

virtual	~ValidityChecker ()
	Destructor. More...

virtual CLFlags &	getFlags () const
	Return the set of command-line flags. More...

virtual void	reprocessFlags ()
	Force reprocessing of all flags. More...

Type-related methods
Methods for creating and looking up types See also class Type
virtual Type	boolType ()
	Create type BOOLEAN. More...

virtual Type	realType ()
	Create type REAL. More...

virtual Type	intType ()
	Create type INT. More...

virtual Type	subrangeType (const Expr &l, const Expr &r)
	Create a subrange type [l..r]. More...

virtual Type	subtypeType (const Expr &pred, const Expr &witness)
	Creates a subtype defined by the given predicate. More...

virtual Type	tupleType (const Type &type0, const Type &type1)
	2-element tuple More...

virtual Type	tupleType (const Type &type0, const Type &type1, const Type &type2)
	3-element tuple More...

virtual Type	tupleType (const std::vector< Type > &types)
	n-element tuple (from a vector of types) More...

virtual Type	recordType (const std::string &field, const Type &type)
	1-element record More...

virtual Type	recordType (const std::string &field0, const Type &type0, const std::string &field1, const Type &type1)
	2-element record More...

virtual Type	recordType (const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2)
	3-element record More...

virtual Type	recordType (const std::vector< std::string > &fields, const std::vector< Type > &types)
	n-element record (fields and types must be of the same length) More...

virtual Type	dataType (const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types)
	Single datatype, single constructor. More...

virtual Type	dataType (const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types)
	Single datatype, multiple constructors. More...

virtual void	dataType (const std::vector< std::string > &names, const std::vector< std::vector< std::string > > &constructors, const std::vector< std::vector< std::vector< std::string > > > &selectors, const std::vector< std::vector< std::vector< Expr > > > &types, std::vector< Type > &returnTypes)
	Multiple datatypes. More...

virtual Type	arrayType (const Type &typeIndex, const Type &typeData)
	Create an array type (ARRAY typeIndex OF typeData) More...

virtual Type	bitvecType (int n)
	Create a bitvector type of length n. More...

virtual Type	funType (const Type &typeDom, const Type &typeRan)
	Create a function type typeDom -> typeRan. More...

virtual Type	funType (const std::vector< Type > &typeDom, const Type &typeRan)
	Create a function type (t1,t2,...,tn) -> typeRan. More...

virtual Type	createType (const std::string &typeName)
	Create named user-defined uninterpreted type. More...

virtual Type	createType (const std::string &typeName, const Type &def)
	Create named user-defined interpreted type (type abbreviation) More...

virtual Type	lookupType (const std::string &typeName)
	Lookup a user-defined (uninterpreted) type by name. Returns Null if none. More...

General Expr methods
See also class Expr class ExprManager
virtual ExprManager *	getEM ()
	Return the ExprManager. More...

virtual Expr	varExpr (const std::string &name, const Type &type)
	Create a variable with a given name and type. More...

virtual Expr	varExpr (const std::string &name, const Type &type, const Expr &def)
	Create a variable with a given name, type, and value. More...

virtual Expr	lookupVar (const std::string &name, Type *type)
	Get the variable associated with a name, and its type. More...

virtual Type	getType (const Expr &e)
	Get the type of the Expr. More...

virtual Type	getBaseType (const Expr &e)
	Get the largest supertype of the Expr. More...

virtual Type	getBaseType (const Type &t)
	Get the largest supertype of the Type. More...

virtual Expr	getTypePred (const Type &t, const Expr &e)
	Get the subtype predicate. More...

virtual Expr	stringExpr (const std::string &str)
	Create a string Expr. More...

virtual Expr	idExpr (const std::string &name)
	Create an ID Expr. More...

virtual Expr	listExpr (const std::vector< Expr > &kids)
	Create a list Expr. More...

virtual Expr	listExpr (const Expr &e1)
	Overloaded version of listExpr with one argument. More...

virtual Expr	listExpr (const Expr &e1, const Expr &e2)
	Overloaded version of listExpr with two arguments. More...

virtual Expr	listExpr (const Expr &e1, const Expr &e2, const Expr &e3)
	Overloaded version of listExpr with three arguments. More...

virtual Expr	listExpr (const std::string &op, const std::vector< Expr > &kids)
	Overloaded version of listExpr with string operator and many arguments. More...

virtual Expr	listExpr (const std::string &op, const Expr &e1)
	Overloaded version of listExpr with string operator and one argument. More...

virtual Expr	listExpr (const std::string &op, const Expr &e1, const Expr &e2)
	Overloaded version of listExpr with string operator and two arguments. More...

virtual Expr	listExpr (const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3)
	Overloaded version of listExpr with string operator and three arguments. More...

virtual void	printExpr (const Expr &e)
	Prints e to the standard output. More...

virtual void	printExpr (const Expr &e, std::ostream &os)
	Prints e to the given ostream. More...

virtual Expr	parseExpr (const Expr &e)
	Parse an expression using a Theory-specific parser. More...

virtual Type	parseType (const Expr &e)
	Parse a type expression using a Theory-specific parser. More...

virtual Expr	importExpr (const Expr &e)
	Import the Expr from another instance of ValidityChecker. More...

virtual Type	importType (const Type &t)
	Import the Type from another instance of ValidityChecker. More...

virtual void	cmdsFromString (const std::string &s, InputLanguage lang=PRESENTATION_LANG)
	Parse a sequence of commands from a presentation language string. More...

virtual Expr	exprFromString (const std::string &e, InputLanguage lang=PRESENTATION_LANG)
	Parse an expression from a presentation language string. More...

Core expression methods
Methods for manipulating core expressions Except for equality and ite, the children provided as arguments must be of type Boolean.
virtual Expr	trueExpr ()
	Return TRUE Expr. More...

virtual Expr	falseExpr ()
	Return FALSE Expr. More...

virtual Expr	notExpr (const Expr &child)
	Create negation. More...

virtual Expr	andExpr (const Expr &left, const Expr &right)
	Create 2-element conjunction. More...

virtual Expr	andExpr (const std::vector< Expr > &children)
	Create n-element conjunction. More...

virtual Expr	orExpr (const Expr &left, const Expr &right)
	Create 2-element disjunction. More...

virtual Expr	orExpr (const std::vector< Expr > &children)
	Create n-element disjunction. More...

virtual Expr	impliesExpr (const Expr &hyp, const Expr &conc)
	Create Boolean implication. More...

virtual Expr	iffExpr (const Expr &left, const Expr &right)
	Create left IFF right (boolean equivalence) More...

virtual Expr	eqExpr (const Expr &child0, const Expr &child1)
	Create an equality expression. More...

virtual Expr	iteExpr (const Expr &ifpart, const Expr &thenpart, const Expr &elsepart)
	Create IF ifpart THEN thenpart ELSE elsepart ENDIF. More...

virtual Expr	distinctExpr (const std::vector< Expr > &children)
	Create an expression asserting that all the children are different. More...

User-defined (uninterpreted) function methods
Methods for manipulating uninterpreted function expressions
virtual Op	createOp (const std::string &name, const Type &type)
	Create a named uninterpreted function with a given type. More...

virtual Op	createOp (const std::string &name, const Type &type, const Expr &def)
	Create a named user-defined function with a given type. More...

virtual Op	lookupOp (const std::string &name, Type *type)
	Get the Op associated with a name, and its type. More...

virtual Expr	funExpr (const Op &op, const Expr &child)
	Unary function application (op must be of function type) More...

virtual Expr	funExpr (const Op &op, const Expr &left, const Expr &right)
	Binary function application (op must be of function type) More...

virtual Expr	funExpr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)
	Ternary function application (op must be of function type) More...

virtual Expr	funExpr (const Op &op, const std::vector< Expr > &children)
	n-ary function application (op must be of function type) More...

Arithmetic expression methods
Methods for manipulating arithmetic expressions These functions create arithmetic expressions. The children provided as arguments must be of type Real.
virtual bool	addPairToArithOrder (const Expr &smaller, const Expr &bigger)

virtual Expr	ratExpr (int n, int d=1)
	Create a rational number with numerator n and denominator d. More...

virtual Expr	ratExpr (const std::string &n, const std::string &d, int base)
	Create a rational number with numerator n and denominator d. More...

virtual Expr	ratExpr (const std::string &n, int base=10)
	Create a rational from a single string. More...

virtual Expr	uminusExpr (const Expr &child)
	Unary minus. More...

virtual Expr	plusExpr (const Expr &left, const Expr &right)
	Create 2-element sum (left + right) More...

virtual Expr	plusExpr (const std::vector< Expr > &children)
	Create n-element sum. More...

virtual Expr	minusExpr (const Expr &left, const Expr &right)
	Make a difference (left - right) More...

virtual Expr	multExpr (const Expr &left, const Expr &right)
	Create a product (left * right) More...

virtual Expr	powExpr (const Expr &x, const Expr &n)
	Create a power expression (x ^ n); n must be integer. More...

virtual Expr	divideExpr (const Expr &numerator, const Expr &denominator)
	Create expression x / y. More...

virtual Expr	ltExpr (const Expr &left, const Expr &right)
	Create (left < right) More...

virtual Expr	leExpr (const Expr &left, const Expr &right)
	Create (left <= right) More...

virtual Expr	gtExpr (const Expr &left, const Expr &right)
	Create (left > right) More...

virtual Expr	geExpr (const Expr &left, const Expr &right)
	Create (left >= right) More...

Record expression methods
Methods for manipulating record expressions
virtual Expr	recordExpr (const std::string &field, const Expr &expr)
	Create a 1-element record value (# field := expr #) More...

virtual Expr	recordExpr (const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1)
	Create a 2-element record value (# field0 := expr0, field1 := expr1 #) More...

virtual Expr	recordExpr (const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2)
	Create a 3-element record value (# field_i := expr_i #) More...

virtual Expr	recordExpr (const std::vector< std::string > &fields, const std::vector< Expr > &exprs)
	Create an n-element record value (# field_i := expr_i #) More...

virtual Expr	recSelectExpr (const Expr &record, const std::string &field)
	Create record.field (field selection) More...

virtual Expr	recUpdateExpr (const Expr &record, const std::string &field, const Expr &newValue)
	Record update; equivalent to "record WITH .field := newValue". More...

Array expression methods
Methods for manipulating array expressions
virtual Expr	readExpr (const Expr &array, const Expr &index)
	Create an expression array[index] (array access) More...

virtual Expr	writeExpr (const Expr &array, const Expr &index, const Expr &newValue)
	Array update; equivalent to "array WITH index := newValue". More...

Bitvector expression methods
Methods for manipulating bitvector expressions
virtual Expr	newBVConstExpr (const std::string &s, int base=2)

virtual Expr	newBVConstExpr (const std::vector< bool > &bits)

virtual Expr	newBVConstExpr (const Rational &r, int len=0)

virtual Expr	newConcatExpr (const Expr &t1, const Expr &t2)

virtual Expr	newConcatExpr (const std::vector< Expr > &kids)

virtual Expr	newBVExtractExpr (const Expr &e, int hi, int low)

virtual Expr	newBVNegExpr (const Expr &t1)

virtual Expr	newBVAndExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVAndExpr (const std::vector< Expr > &kids)

virtual Expr	newBVOrExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVOrExpr (const std::vector< Expr > &kids)

virtual Expr	newBVXorExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVXorExpr (const std::vector< Expr > &kids)

virtual Expr	newBVXnorExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVXnorExpr (const std::vector< Expr > &kids)

virtual Expr	newBVNandExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVNorExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVCompExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVLTExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVLEExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVSLTExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVSLEExpr (const Expr &t1, const Expr &t2)

virtual Expr	newSXExpr (const Expr &t1, int len)

virtual Expr	newBVUminusExpr (const Expr &t1)

virtual Expr	newBVSubExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVPlusExpr (int numbits, const std::vector< Expr > &k)
	'numbits' is the number of bits in the result More...

virtual Expr	newBVPlusExpr (int numbits, const Expr &t1, const Expr &t2)

virtual Expr	newBVMultExpr (int numbits, const Expr &t1, const Expr &t2)

virtual Expr	newBVUDivExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVURemExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVSDivExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVSRemExpr (const Expr &t1, const Expr &t2)

virtual Expr	newBVSModExpr (const Expr &t1, const Expr &t2)

virtual Expr	newFixedLeftShiftExpr (const Expr &t1, int r)

virtual Expr	newFixedConstWidthLeftShiftExpr (const Expr &t1, int r)

virtual Expr	newFixedRightShiftExpr (const Expr &t1, int r)

virtual Expr	newBVSHL (const Expr &t1, const Expr &t2)

virtual Expr	newBVLSHR (const Expr &t1, const Expr &t2)

virtual Expr	newBVASHR (const Expr &t1, const Expr &t2)

virtual Rational	computeBVConst (const Expr &e)

Other expression methods
Methods for manipulating other kinds of expressions
virtual Expr	tupleExpr (const std::vector< Expr > &exprs)
	Tuple expression. More...

virtual Expr	tupleSelectExpr (const Expr &tuple, int index)
	Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5) More...

virtual Expr	tupleUpdateExpr (const Expr &tuple, int index, const Expr &newValue)
	Tuple update; equivalent to "tuple WITH index := newValue". More...

virtual Expr	datatypeConsExpr (const std::string &constructor, const std::vector< Expr > &args)
	Datatype constructor expression. More...

virtual Expr	datatypeSelExpr (const std::string &selector, const Expr &arg)
	Datatype selector expression. More...

virtual Expr	datatypeTestExpr (const std::string &constructor, const Expr &arg)
	Datatype tester expression. More...

virtual Expr	boundVarExpr (const std::string &name, const std::string &uid, const Type &type)
	Create a bound variable with a given name, unique ID (uid) and type. More...

virtual Expr	forallExpr (const std::vector< Expr > &vars, const Expr &body)
	Universal quantifier. More...

virtual Expr	forallExpr (const std::vector< Expr > &vars, const Expr &body, const Expr &trigger)
	Universal quantifier with a trigger. More...

virtual Expr	forallExpr (const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers)
	Universal quantifier with a set of triggers. More...

virtual Expr	forallExpr (const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers)
	Universal quantifier with a set of multi-triggers. More...

virtual void	setTriggers (const Expr &e, const std::vector< std::vector< Expr > > &triggers)
	Set triggers for quantifier instantiation. More...

virtual void	setTriggers (const Expr &e, const std::vector< Expr > &triggers)
	Set triggers for quantifier instantiation (no multi-triggers) More...

virtual void	setTrigger (const Expr &e, const Expr &trigger)
	Set a single trigger for quantifier instantiation. More...

virtual void	setMultiTrigger (const Expr &e, const std::vector< Expr > &multiTrigger)
	Set a single multi-trigger for quantifier instantiation. More...

virtual Expr	existsExpr (const std::vector< Expr > &vars, const Expr &body)
	Existential quantifier. More...

virtual Op	lambdaExpr (const std::vector< Expr > &vars, const Expr &body)
	Lambda-expression. More...

virtual Op	transClosure (const Op &op)
	Transitive closure of a binary predicate. More...

virtual Expr	simulateExpr (const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n)
	Symbolic simulation expression. More...

Validity checking methods
Methods related to validity checking This group includes methods for asserting formulas, checking validity in the given logical context, manipulating the scope level of the context, etc.
virtual void	setResourceLimit (unsigned limit)
	Set the resource limit (0==unlimited, 1==exhausted). More...

virtual void	setTimeLimit (unsigned limit)
	Set a time limit in tenth of a second,. More...

virtual void	assertFormula (const Expr &e)
	Assert a new formula in the current context. More...

virtual void	registerAtom (const Expr &e)
	Register an atomic formula of interest. More...

virtual Expr	getImpliedLiteral ()
	Return next literal implied by last assertion. Null Expr if none. More...

virtual Expr	simplify (const Expr &e)
	Simplify e with respect to the current context. More...

virtual QueryResult	query (const Expr &e)
	Check validity of e in the current context. More...

virtual QueryResult	checkUnsat (const Expr &e)
	Check satisfiability of the expr in the current context. More...

virtual QueryResult	checkContinue ()
	Get the next model. More...

virtual QueryResult	restart (const Expr &e)
	Restart the most recent query with e as an additional assertion. More...

virtual void	returnFromCheck ()
	Returns to context immediately before last invalid query. More...

virtual void	getUserAssumptions (std::vector< Expr > &assumptions)
	Get assumptions made by the user in this and all previous contexts. More...

virtual void	getInternalAssumptions (std::vector< Expr > &assumptions)
	Get assumptions made internally in this and all previous contexts. More...

virtual void	getAssumptions (std::vector< Expr > &assumptions)
	Get all assumptions made in this and all previous contexts. More...

virtual void	getAssumptionsUsed (std::vector< Expr > &assumptions)
	Returns the set of assumptions used in the proof of queried formula. More...

virtual Expr	getProofQuery ()

virtual void	getCounterExample (std::vector< Expr > &assumptions, bool inOrder=true)
	Return the internal assumptions that make the queried formula false. More...

virtual void	getConcreteModel (ExprMap< Expr > &m)
	Will assign concrete values to all user created variables. More...

virtual QueryResult	tryModelGeneration ()
	If the result of the last query was UNKNOWN try to actually build the model to verify the result. More...

virtual FormulaValue	value (const Expr &e)

virtual bool	inconsistent (std::vector< Expr > &assumptions)
	Returns true if the current context is inconsistent. More...

virtual bool	inconsistent ()
	Returns true if the current context is inconsistent. More...

virtual bool	incomplete ()
	Returns true if the invalid result from last query() is imprecise. More...

virtual bool	incomplete (std::vector< std::string > &reasons)
	Returns true if the invalid result from last query() is imprecise. More...

virtual Proof	getProof ()
	Returns the proof term for the last proven query. More...

virtual Expr	getValue (const Expr &e)
	Evaluate an expression and return a concrete value in the model. More...

virtual Expr	getTCC ()
	Returns the TCC of the last assumption or query. More...

virtual void	getAssumptionsTCC (std::vector< Expr > &assumptions)
	Return the set of assumptions used in the proof of the last TCC. More...

virtual Proof	getProofTCC ()
	Returns the proof of TCC of the last assumption or query. More...

virtual Expr	getClosure ()
	After successful query, return its closure \|- Gamma => phi. More...

virtual Proof	getProofClosure ()
	Construct a proof of the query closure \|- Gamma => phi. More...

Context methods
Methods for manipulating contexts Contexts support stack-based push and pop. There are two separate notions of the current context stack. stackLevel(), push(), pop(), and popto() work with the user-level notion of the stack. scopeLevel(), pushScope(), popScope(), and poptoScope() work with the internal stack which is more fine-grained than the user stack. Do not use the scope methods unless you know what you are doing.
virtual int	stackLevel ()
	Returns the current stack level. Initial level is 0. More...

virtual void	push ()
	Checkpoint the current context and increase the scope level. More...

virtual void	pop ()
	Restore the current context to its state at the last checkpoint. More...

virtual void	popto (int stackLevel)
	Restore the current context to the given stackLevel. More...

virtual int	scopeLevel ()
	Returns the current scope level. Initially, the scope level is 1. More...

virtual void	pushScope ()
	Checkpoint the current context and increase the internal scope level. Do not use unless you know what you're doing! More...

virtual void	popScope ()
	Restore the current context to its state at the last internal checkpoint. Do not use unless you know what you're doing! More...

virtual void	poptoScope (int scopeLevel)
	Restore the current context to the given scopeLevel. More...

virtual Context *	getCurrentContext ()
	Get the current context. More...

virtual void	reset ()
	Destroy and recreate validity checker: resets everything except for flags. More...

virtual void	logAnnotation (const Expr &annot)
	Add an annotation to the current script - prints annot when translating. More...

Reading files
Methods for reading external files
virtual void	loadFile (const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false)
	Read and execute the commands from a file given by name ("" means stdin) More...

virtual void	loadFile (std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false)
	Read and execute the commands from a stream. More...

Reporting Statistics
Methods for collecting and reporting run-time statistics
virtual Statistics	getStatistics ()
	Get statistics object. More...

virtual void	printStatistics ()
	Print collected statistics to stdout. More...

Static Public Member Functions
static CLFlags	createFlags ()
	Create the set of command line flags with default values;. More...

static ValidityChecker *	create (const CLFlags &flags)
	Create an instance of ValidityChecker. More...

static ValidityChecker *	create ()
	Create an instance of ValidityChecker using default flag values. More...

Friends
class	Type

Detailed Description

CVC3 API (compatibility layer for CVC4)

All terms and formulas are represented as expressions using the Expr class. The notion of a context is also important. A context is a "background" set of formulas which are assumed to be true or false. Formulas can be added to the context explicitly, using assertFormula, or they may be added as part of processing a query command. At any time, the current set of formulas making up the context can be retrieved using getAssumptions.

Definition at line 514 of file cvc3_compat.h.

Constructor & Destructor Documentation

CVC3::ValidityChecker::ValidityChecker ( )

Constructor.

virtual CVC3::ValidityChecker::~ValidityChecker ( )

virtual

Destructor.

Member Function Documentation

virtual bool CVC3::ValidityChecker::addPairToArithOrder	(	const Expr &	smaller,
		const Expr &	bigger
	)

virtual

Add the pair of variables to the variable ordering for aritmetic solving. Terms that are not arithmetic will be ignored.

Parameters

smaller	the smaller variable
bigger	the bigger variable

virtual Expr CVC3::ValidityChecker::andExpr	(	const Expr &	left,
		const Expr &	right
	)

virtual

Create 2-element conjunction.

virtual Expr CVC3::ValidityChecker::andExpr ( const std::vector< Expr > & children )

virtual

Create n-element conjunction.

virtual Type CVC3::ValidityChecker::arrayType	(	const Type &	typeIndex,
		const Type &	typeData
	)

virtual

Create an array type (ARRAY typeIndex OF typeData)

virtual void CVC3::ValidityChecker::assertFormula ( const Expr & e )

virtual

Assert a new formula in the current context.

This creates the assumption e |- e. The formula must have Boolean type.

virtual Type CVC3::ValidityChecker::bitvecType ( int n )

virtual

Create a bitvector type of length n.

virtual Type CVC3::ValidityChecker::boolType ( )

virtual

Create type BOOLEAN.

virtual Expr CVC3::ValidityChecker::boundVarExpr	(	const std::string &	name,
		const std::string &	uid,
		const Type &	type
	)

virtual

Create a bound variable with a given name, unique ID (uid) and type.

Parameters

name	is the name of the variable
uid	is the unique ID (a string), which must be unique for each variable
type	is its type. The type cannot be a function type.

Returns: an Expr representation of a new variable

virtual QueryResult CVC3::ValidityChecker::checkContinue ( )

virtual

Get the next model.

This method should only be called after a query which returns INVALID. Its return values are as for query().

virtual QueryResult CVC3::ValidityChecker::checkUnsat ( const Expr & e )

virtual

Check satisfiability of the expr in the current context.

Equivalent to query(!e)

virtual void CVC3::ValidityChecker::cmdsFromString	(	const std::string &	s,
		InputLanguage	lang = `PRESENTATION_LANG`
	)

virtual

Parse a sequence of commands from a presentation language string.

virtual Rational CVC3::ValidityChecker::computeBVConst ( const Expr & e )

virtual

static ValidityChecker* CVC3::ValidityChecker::create ( const CLFlags & flags )

static

Create an instance of ValidityChecker.

Parameters

flags is the set of command line flags.

static ValidityChecker* CVC3::ValidityChecker::create ( )

static

Create an instance of ValidityChecker using default flag values.

static CLFlags CVC3::ValidityChecker::createFlags ( )

static

Create the set of command line flags with default values;.

Returns: the set of flags by value

virtual Op CVC3::ValidityChecker::createOp	(	const std::string &	name,
		const Type &	type
	)

virtual

Create a named uninterpreted function with a given type.

Parameters

name	is the new function's name (as ID Expr)
type	is a function type ( [range -> domain] )

virtual Op CVC3::ValidityChecker::createOp	(	const std::string &	name,
		const Type &	type,
		const Expr &	def
	)

virtual

Create a named user-defined function with a given type.

virtual Type CVC3::ValidityChecker::createType ( const std::string & typeName )

virtual

Create named user-defined uninterpreted type.

virtual Type CVC3::ValidityChecker::createType	(	const std::string &	typeName,
		const Type &	def
	)

virtual

Create named user-defined interpreted type (type abbreviation)

virtual Type CVC3::ValidityChecker::dataType	(	const std::string &	name,
		const std::string &	constructor,
		const std::vector< std::string > &	selectors,
		const std::vector< Expr > &	types
	)

virtual

Single datatype, single constructor.

The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.

virtual Type CVC3::ValidityChecker::dataType	(	const std::string &	name,
		const std::vector< std::string > &	constructors,
		const std::vector< std::vector< std::string > > &	selectors,
		const std::vector< std::vector< Expr > > &	types
	)

virtual

Single datatype, multiple constructors.

The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.

virtual void CVC3::ValidityChecker::dataType	(	const std::vector< std::string > &	names,
		const std::vector< std::vector< std::string > > &	constructors,
		const std::vector< std::vector< std::vector< std::string > > > &	selectors,
		const std::vector< std::vector< std::vector< Expr > > > &	types,
		std::vector< Type > &	returnTypes
	)

virtual

Multiple datatypes.

The types are either type exressions (obtained from a type with getExpr()) or string expressions containing the name of (one of) the dataType(s) being defined.

virtual Expr CVC3::ValidityChecker::datatypeConsExpr	(	const std::string &	constructor,
		const std::vector< Expr > &	args
	)

virtual

Datatype constructor expression.

virtual Expr CVC3::ValidityChecker::datatypeSelExpr	(	const std::string &	selector,
		const Expr &	arg
	)

virtual

Datatype selector expression.

virtual Expr CVC3::ValidityChecker::datatypeTestExpr	(	const std::string &	constructor,
		const Expr &	arg
	)

virtual

Datatype tester expression.

virtual Expr CVC3::ValidityChecker::distinctExpr ( const std::vector< Expr > & children )

virtual

Create an expression asserting that all the children are different.

Parameters

children the children to be asserted different

virtual Expr CVC3::ValidityChecker::divideExpr	(	const Expr &	numerator,
		const Expr &	denominator
	)

virtual

Create expression x / y.

virtual Expr CVC3::ValidityChecker::eqExpr	(	const Expr &	child0,
		const Expr &	child1
	)

virtual

Create an equality expression.

The two children must have the same type, and cannot be of type Boolean.

virtual Expr CVC3::ValidityChecker::existsExpr	(	const std::vector< Expr > &	vars,
		const Expr &	body
	)

virtual

Existential quantifier.

virtual Expr CVC3::ValidityChecker::exprFromString	(	const std::string &	e,
		InputLanguage	lang = `PRESENTATION_LANG`
	)

virtual

Parse an expression from a presentation language string.

Only PRESENTATION_LANG and SMTLIB_V2_LANG are supported. Any other value for lang will raise an exception.

virtual Expr CVC3::ValidityChecker::falseExpr ( )

virtual

Return FALSE Expr.

virtual Expr CVC3::ValidityChecker::forallExpr	(	const std::vector< Expr > &	vars,
		const Expr &	body
	)

virtual

Universal quantifier.

virtual Expr CVC3::ValidityChecker::forallExpr	(	const std::vector< Expr > &	vars,
		const Expr &	body,
		const Expr &	trigger
	)

virtual

Universal quantifier with a trigger.

virtual Expr CVC3::ValidityChecker::forallExpr	(	const std::vector< Expr > &	vars,
		const Expr &	body,
		const std::vector< Expr > &	triggers
	)

virtual

Universal quantifier with a set of triggers.

virtual Expr CVC3::ValidityChecker::forallExpr	(	const std::vector< Expr > &	vars,
		const Expr &	body,
		const std::vector< std::vector< Expr > > &	triggers
	)

virtual

Universal quantifier with a set of multi-triggers.

virtual Expr CVC3::ValidityChecker::funExpr	(	const Op &	op,
		const Expr &	child
	)

virtual

Unary function application (op must be of function type)

virtual Expr CVC3::ValidityChecker::funExpr	(	const Op &	op,
		const Expr &	left,
		const Expr &	right
	)

virtual

Binary function application (op must be of function type)

virtual Expr CVC3::ValidityChecker::funExpr	(	const Op &	op,
		const Expr &	child0,
		const Expr &	child1,
		const Expr &	child2
	)

virtual

Ternary function application (op must be of function type)

virtual Expr CVC3::ValidityChecker::funExpr	(	const Op &	op,
		const std::vector< Expr > &	children
	)

virtual

n-ary function application (op must be of function type)

virtual Type CVC3::ValidityChecker::funType	(	const Type &	typeDom,
		const Type &	typeRan
	)

virtual

Create a function type typeDom -> typeRan.

virtual Type CVC3::ValidityChecker::funType	(	const std::vector< Type > &	typeDom,
		const Type &	typeRan
	)

virtual

Create a function type (t1,t2,...,tn) -> typeRan.

virtual Expr CVC3::ValidityChecker::geExpr	(	const Expr &	left,
		const Expr &	right
	)

virtual

Create (left >= right)

virtual void CVC3::ValidityChecker::getAssumptions ( std::vector< Expr > & assumptions )

virtual

Get all assumptions made in this and all previous contexts.

Parameters

assumptions should be empty on entry.

virtual void CVC3::ValidityChecker::getAssumptionsTCC ( std::vector< Expr > & assumptions )

virtual

Return the set of assumptions used in the proof of the last TCC.

virtual void CVC3::ValidityChecker::getAssumptionsUsed ( std::vector< Expr > & assumptions )

virtual

Returns the set of assumptions used in the proof of queried formula.

It returns a subset of getAssumptions(). If the last query was false or there has not yet been a query, it does nothing. NOTE: this functionality is not supported yet

Parameters

assumptions should be empty on entry.

virtual Type CVC3::ValidityChecker::getBaseType ( const Expr & e )

virtual

Get the largest supertype of the Expr.

virtual Type CVC3::ValidityChecker::getBaseType ( const Type & t )

virtual

Get the largest supertype of the Type.

virtual Expr CVC3::ValidityChecker::getClosure ( )

virtual

After successful query, return its closure |- Gamma => phi.

Turn a valid query Gamma |- phi into an implication |- Gamma => phi.

Returns Null if last query was invalid.

virtual void CVC3::ValidityChecker::getConcreteModel ( ExprMap< Expr > & m )

virtual

Will assign concrete values to all user created variables.

This function should only be called after a query which return false.

virtual void CVC3::ValidityChecker::getCounterExample	(	std::vector< Expr > &	assumptions,
		bool	inOrder = `true`
	)

virtual

Return the internal assumptions that make the queried formula false.

This method should only be called after a query which returns false. It will try to return the simplest possible subset of the internal assumptions sufficient to make the queried expression false.

Parameters

assumptions	should be empty on entry.
inOrder	if true, returns the assumptions in the order they were made. This is slightly more expensive than inOrder = false.

virtual Context* CVC3::ValidityChecker::getCurrentContext ( )

virtual

Get the current context.

virtual ExprManager* CVC3::ValidityChecker::getEM ( )

virtual

Return the ExprManager.

virtual CLFlags& CVC3::ValidityChecker::getFlags ( ) const

virtual

Return the set of command-line flags.

The flags are returned by reference, and if modified, will have an immediate effect on the subsequent commands. Note that not all flags will have such an effect; some flags are used only at initialization time (like "sat"), and therefore, will not take effect if modified after ValidityChecker is created.

virtual Expr CVC3::ValidityChecker::getImpliedLiteral ( )

virtual

Return next literal implied by last assertion. Null Expr if none.

Returned literals are either registered atomic formulas or their negation

virtual void CVC3::ValidityChecker::getInternalAssumptions ( std::vector< Expr > & assumptions )

virtual

Get assumptions made internally in this and all previous contexts.

Internal assumptions are literals assumed by the sat solver.

Parameters

assumptions should be empty on entry.

virtual Proof CVC3::ValidityChecker::getProof ( )

virtual

Returns the proof term for the last proven query.

If there has not been a successful query, it should return a NULL proof

virtual Proof CVC3::ValidityChecker::getProofClosure ( )

virtual

Construct a proof of the query closure |- Gamma => phi.

Returns Null if last query was Invalid.

virtual Expr CVC3::ValidityChecker::getProofQuery ( )

virtual

virtual Proof CVC3::ValidityChecker::getProofTCC ( )

virtual

Returns the proof of TCC of the last assumption or query.

Returns Null if no assumptions or queries were performed.

virtual Statistics CVC3::ValidityChecker::getStatistics ( )

virtual

Get statistics object.

virtual Expr CVC3::ValidityChecker::getTCC ( )

virtual

Returns the TCC of the last assumption or query.

Returns Null if no assumptions or queries were performed.

virtual Type CVC3::ValidityChecker::getType ( const Expr & e )

virtual

Get the type of the Expr.

virtual Expr CVC3::ValidityChecker::getTypePred	(	const Type &	t,
		const Expr &	e
	)

virtual

Get the subtype predicate.

virtual void CVC3::ValidityChecker::getUserAssumptions ( std::vector< Expr > & assumptions )

virtual

Get assumptions made by the user in this and all previous contexts.

User assumptions are created either by calls to assertFormula or by a call to query. In the latter case, the negated query is added as an assumption.

Parameters

assumptions should be empty on entry.

virtual Expr CVC3::ValidityChecker::getValue ( const Expr & e )

virtual

Evaluate an expression and return a concrete value in the model.

If the last query was not invalid, should return NULL expr

virtual Expr CVC3::ValidityChecker::gtExpr	(	const Expr &	left,
		const Expr &	right
	)

virtual

Create (left > right)

virtual Expr CVC3::ValidityChecker::idExpr ( const std::string & name )

virtual

Create an ID Expr.

virtual Expr CVC3::ValidityChecker::iffExpr	(	const Expr &	left,
		const Expr &	right
	)

virtual

Create left IFF right (boolean equivalence)

virtual Expr CVC3::ValidityChecker::impliesExpr	(	const Expr &	hyp,
		const Expr &	conc
	)

virtual

Create Boolean implication.

virtual Expr CVC3::ValidityChecker::importExpr ( const Expr & e )

virtual

Import the Expr from another instance of ValidityChecker.

When expressions need to be passed among several instances of ValidityChecker, they need to be explicitly imported into the corresponding instance using this method. The return result is an identical expression that belongs to the current instance of ValidityChecker, and can be safely used as part of more complex expressions from the same instance.

virtual Type CVC3::ValidityChecker::importType ( const Type & t )

virtual

Import the Type from another instance of ValidityChecker.

See also: getType()

virtual bool CVC3::ValidityChecker::incomplete ( )

virtual

Returns true if the invalid result from last query() is imprecise.

Some decision procedures in CVC are incomplete (quantifier elimination, non-linear arithmetic, etc.). If any incomplete features were used during the last query(), and the result is "invalid" (query() returns false), then this result is inconclusive. It means that the system gave up the search for contradiction at some point.

virtual bool CVC3::ValidityChecker::incomplete ( std::vector< std::string > & reasons )

virtual

Returns true if the invalid result from last query() is imprecise.

See also: incomplete()

The argument is filled with the reasons for incompleteness (they are intended to be shown to the end user).

virtual bool CVC3::ValidityChecker::inconsistent ( std::vector< Expr > & assumptions )

virtual

Returns true if the current context is inconsistent.

Also returns a minimal set of assertions used to determine the inconsistency.

Parameters

assumptions should be empty on entry.

virtual bool CVC3::ValidityChecker::inconsistent ( )

virtual

Returns true if the current context is inconsistent.

virtual Type CVC3::ValidityChecker::intType ( )

virtual

Create type INT.

virtual Expr CVC3::ValidityChecker::iteExpr	(	const Expr &	ifpart,
		const Expr &	thenpart,
		const Expr &	elsepart
	)

virtual

Create IF ifpart THEN thenpart ELSE elsepart ENDIF.

Parameters

ifpart	must be of type Boolean.
thenpart	and
elsepart	must have the same type, which will also be the type of the ite expression.

virtual Op CVC3::ValidityChecker::lambdaExpr	(	const std::vector< Expr > &	vars,
		const Expr &	body
	)

virtual

Lambda-expression.

virtual Expr CVC3::ValidityChecker::leExpr	(	const Expr &	left,
		const Expr &	right
	)

virtual

Create (left <= right)

virtual Expr CVC3::ValidityChecker::listExpr ( const std::vector< Expr > & kids )

virtual

Create a list Expr.

Intermediate representation for DP-specific expressions. Normally, the first element of the list is a string Expr representing an operator, and the rest of the list are the arguments. For example,

kids.push_back(vc->stringExpr("PLUS")); kids.push_back(x); // x and y are previously created Exprs kids.push_back(y); Expr lst = vc->listExpr(kids);

Or, alternatively (using its overloaded version):

Expr lst = vc->listExpr("PLUS", x, y);

or

vector<Expr> summands; summands.push_back(x); summands.push_back(y); ... Expr lst = vc->listExpr("PLUS", summands);

virtual Expr CVC3::ValidityChecker::listExpr ( const Expr & e1 )

virtual

Overloaded version of listExpr with one argument.

virtual Expr CVC3::ValidityChecker::listExpr	(	const Expr &	e1,
		const Expr &	e2
	)

virtual

Overloaded version of listExpr with two arguments.

virtual Expr CVC3::ValidityChecker::listExpr	(	const Expr &	e1,
		const Expr &	e2,
		const Expr &	e3
	)

virtual

Overloaded version of listExpr with three arguments.

virtual Expr CVC3::ValidityChecker::listExpr	(	const std::string &	op,
		const std::vector< Expr > &	kids
	)

virtual

Overloaded version of listExpr with string operator and many arguments.

virtual Expr CVC3::ValidityChecker::listExpr	(	const std::string &	op,
		const Expr &	e1
	)

virtual

Overloaded version of listExpr with string operator and one argument.

virtual Expr CVC3::ValidityChecker::listExpr	(	const std::string &	op,
		const Expr &	e1,
		const Expr &	e2
	)

virtual

Overloaded version of listExpr with string operator and two arguments.

virtual Expr CVC3::ValidityChecker::listExpr	(	const std::string &	op,
		const Expr &	e1,
		const Expr &	e2,
		const Expr &	e3
	)

virtual

Overloaded version of listExpr with string operator and three arguments.

virtual void CVC3::ValidityChecker::loadFile	(	const std::string &	fileName,
		InputLanguage	lang = `PRESENTATION_LANG`,
		bool	interactive = `false`,
		bool	calledFromParser = `false`
	)

virtual

Read and execute the commands from a file given by name ("" means stdin)

virtual void CVC3::ValidityChecker::loadFile	(	std::istream &	is,
		InputLanguage	lang = `PRESENTATION_LANG`,
		bool	interactive = `false`
	)

virtual

Read and execute the commands from a stream.

virtual void CVC3::ValidityChecker::logAnnotation ( const Expr & annot )

virtual

Add an annotation to the current script - prints annot when translating.

virtual Op CVC3::ValidityChecker::lookupOp	(	const std::string &	name,
		Type *	type
	)

virtual

Get the Op associated with a name, and its type.

Parameters

name	is the operator name
type	is where the type value is returned

Returns: an Op by the name. If there is no such Op, a NULL \ Op is returned.

virtual Type CVC3::ValidityChecker::lookupType ( const std::string & typeName )

virtual

Lookup a user-defined (uninterpreted) type by name. Returns Null if none.

virtual Expr CVC3::ValidityChecker::lookupVar	(	const std::string &	name,
		Type *	type
	)

virtual

Get the variable associated with a name, and its type.

Parameters

name	is the variable name
type	is where the type value is returned

Returns: a variable by the name. If there is no such Expr, a NULL \ Expr is returned.

virtual Expr CVC3::ValidityChecker::ltExpr	(	const Expr &	left,
		const Expr &	right
	)

virtual

Create (left < right)

virtual Expr CVC3::ValidityChecker::minusExpr	(	const Expr &	left,
		const Expr &	right
	)

virtual

Make a difference (left - right)

virtual Expr CVC3::ValidityChecker::multExpr	(	const Expr &	left,
		const Expr &	right
	)

virtual

Create a product (left * right)

virtual Expr CVC3::ValidityChecker::newBVAndExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVAndExpr ( const std::vector< Expr > & kids )

virtual

virtual Expr CVC3::ValidityChecker::newBVASHR	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVCompExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVConstExpr	(	const std::string &	s,
		int	base = `2`
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVConstExpr ( const std::vector< bool > & bits )

virtual

virtual Expr CVC3::ValidityChecker::newBVConstExpr	(	const Rational &	r,
		int	len = `0`
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVExtractExpr	(	const Expr &	e,
		int	hi,
		int	low
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVLEExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVLSHR	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVLTExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVMultExpr	(	int	numbits,
		const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVNandExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVNegExpr ( const Expr & t1 )

virtual

virtual Expr CVC3::ValidityChecker::newBVNorExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVOrExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVOrExpr ( const std::vector< Expr > & kids )

virtual

virtual Expr CVC3::ValidityChecker::newBVPlusExpr	(	int	numbits,
		const std::vector< Expr > &	k
	)

virtual

'numbits' is the number of bits in the result

virtual Expr CVC3::ValidityChecker::newBVPlusExpr	(	int	numbits,
		const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVSDivExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVSHL	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVSLEExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVSLTExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVSModExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVSRemExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVSubExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVUDivExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVUminusExpr ( const Expr & t1 )

virtual

virtual Expr CVC3::ValidityChecker::newBVURemExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVXnorExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVXnorExpr ( const std::vector< Expr > & kids )

virtual

virtual Expr CVC3::ValidityChecker::newBVXorExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newBVXorExpr ( const std::vector< Expr > & kids )

virtual

virtual Expr CVC3::ValidityChecker::newConcatExpr	(	const Expr &	t1,
		const Expr &	t2
	)

virtual

virtual Expr CVC3::ValidityChecker::newConcatExpr ( const std::vector< Expr > & kids )

virtual

virtual Expr CVC3::ValidityChecker::newFixedConstWidthLeftShiftExpr	(	const Expr &	t1,
		int	r
	)

virtual

virtual Expr CVC3::ValidityChecker::newFixedLeftShiftExpr	(	const Expr &	t1,
		int	r
	)

virtual

virtual Expr CVC3::ValidityChecker::newFixedRightShiftExpr	(	const Expr &	t1,
		int	r
	)

virtual

virtual Expr CVC3::ValidityChecker::newSXExpr	(	const Expr &	t1,
		int	len
	)

virtual

virtual Expr CVC3::ValidityChecker::notExpr ( const Expr & child )

virtual

Create negation.

virtual Expr CVC3::ValidityChecker::orExpr	(	const Expr &	left,
		const Expr &	right
	)

virtual

Create 2-element disjunction.

virtual Expr CVC3::ValidityChecker::orExpr ( const std::vector< Expr > & children )

virtual

Create n-element disjunction.

virtual Expr CVC3::ValidityChecker::parseExpr ( const Expr & e )

virtual

Parse an expression using a Theory-specific parser.

virtual Type CVC3::ValidityChecker::parseType ( const Expr & e )

virtual

Parse a type expression using a Theory-specific parser.

virtual Expr CVC3::ValidityChecker::plusExpr	(	const Expr &	left,
		const Expr &	right
	)

virtual

Create 2-element sum (left + right)

virtual Expr CVC3::ValidityChecker::plusExpr ( const std::vector< Expr > & children )

virtual

Create n-element sum.

virtual void CVC3::ValidityChecker::pop ( )

virtual

Restore the current context to its state at the last checkpoint.

virtual void CVC3::ValidityChecker::popScope ( )

virtual

Restore the current context to its state at the last internal checkpoint. Do not use unless you know what you're doing!

virtual void CVC3::ValidityChecker::popto ( int stackLevel )

virtual

Restore the current context to the given stackLevel.

Parameters

stackLevel should be greater than or equal to 0 and less than or equal to the current scope level.

virtual void CVC3::ValidityChecker::poptoScope ( int scopeLevel )

virtual

Restore the current context to the given scopeLevel.

Parameters

scopeLevel should be less than or equal to the current scope level.

If scopeLevel is less than 1, then the current context is reset and the scope level is set to 1.

virtual Expr CVC3::ValidityChecker::powExpr	(	const Expr &	x,
		const Expr &	n
	)

virtual

Create a power expression (x ^ n); n must be integer.

virtual void CVC3::ValidityChecker::printExpr ( const Expr & e )

virtual

Prints e to the standard output.

virtual void CVC3::ValidityChecker::printExpr	(	const Expr &	e,
		std::ostream &	os
	)

virtual

Prints e to the given ostream.

virtual void CVC3::ValidityChecker::printStatistics ( )

virtual

Print collected statistics to stdout.

virtual void CVC3::ValidityChecker::push ( )

virtual

Checkpoint the current context and increase the scope level.

virtual void CVC3::ValidityChecker::pushScope ( )

virtual

Checkpoint the current context and increase the internal scope level. Do not use unless you know what you're doing!

virtual QueryResult CVC3::ValidityChecker::query ( const Expr & e )

virtual

Check validity of e in the current context.

If it returns VALID, the scope and context are the same as when called. If it returns INVALID, the context will be one which falsifies the query. If it returns UNKNOWN, the context will falsify the query, but the context may be inconsistent. Finally, if it returns ABORT, the context will be one which satisfies as much as possible.

Parameters

e	is the queried formula

virtual Expr CVC3::ValidityChecker::ratExpr	(	int	n,
		int	d = `1`
	)

virtual

Create a rational number with numerator n and denominator d.

Parameters

n	the numerator
d	the denominator, cannot be 0.

virtual Expr CVC3::ValidityChecker::ratExpr	(	const std::string &	n,
		const std::string &	d,
		int	base
	)

virtual

Create a rational number with numerator n and denominator d.

Here n and d are given as strings. They are converted to arbitrary-precision integers according to the given base.

virtual Expr CVC3::ValidityChecker::ratExpr	(	const std::string &	n,
		int	base = `10`
	)

virtual

Create a rational from a single string.

Parameters

n	can be a string containing an integer, a pair of integers "nnn/ddd", or a number in the fixed or floating point format.
base	is the base in which to interpret the string.

virtual Expr CVC3::ValidityChecker::readExpr	(	const Expr &	array,
		const Expr &	index
	)

virtual

Create an expression array[index] (array access)

Create an expression for the value of array at the given index

virtual Type CVC3::ValidityChecker::realType ( )

virtual

Create type REAL.

virtual Expr CVC3::ValidityChecker::recordExpr	(	const std::string &	field,
		const Expr &	expr
	)

virtual

Create a 1-element record value (# field := expr #)

Fields will be sorted automatically

virtual Expr CVC3::ValidityChecker::recordExpr	(	const std::string &	field0,
		const Expr &	expr0,
		const std::string &	field1,
		const Expr &	expr1
	)

virtual

Create a 2-element record value (# field0 := expr0, field1 := expr1 #)

Fields will be sorted automatically

virtual Expr CVC3::ValidityChecker::recordExpr	(	const std::string &	field0,
		const Expr &	expr0,
		const std::string &	field1,
		const Expr &	expr1,
		const std::string &	field2,
		const Expr &	expr2
	)

virtual

Create a 3-element record value (# field_i := expr_i #)

Fields will be sorted automatically

virtual Expr CVC3::ValidityChecker::recordExpr	(	const std::vector< std::string > &	fields,
		const std::vector< Expr > &	exprs
	)

virtual

Create an n-element record value (# field_i := expr_i #)

Parameters

fields
exprs	must be the same length as fields

Fields will be sorted automatically

virtual Type CVC3::ValidityChecker::recordType	(	const std::string &	field,
		const Type &	type
	)

virtual

1-element record

virtual Type CVC3::ValidityChecker::recordType	(	const std::string &	field0,
		const Type &	type0,
		const std::string &	field1,
		const Type &	type1
	)

virtual

2-element record

Fields will be sorted automatically

virtual Type CVC3::ValidityChecker::recordType	(	const std::string &	field0,
		const Type &	type0,
		const std::string &	field1,
		const Type &	type1,
		const std::string &	field2,
		const Type &	type2
	)

virtual

3-element record

Fields will be sorted automatically

virtual Type CVC3::ValidityChecker::recordType	(	const std::vector< std::string > &	fields,
		const std::vector< Type > &	types
	)

virtual

n-element record (fields and types must be of the same length)

Fields will be sorted automatically

virtual Expr CVC3::ValidityChecker::recSelectExpr	(	const Expr &	record,
		const std::string &	field
	)

virtual

Create record.field (field selection)

Create an expression representing the selection of a field from a record.

virtual Expr CVC3::ValidityChecker::recUpdateExpr	(	const Expr &	record,
		const std::string &	field,
		const Expr &	newValue
	)

virtual

Record update; equivalent to "record WITH .field := newValue".

Notice the `.' before field in the presentation language (and the comment above); this is to distinguish it from datatype update.

virtual void CVC3::ValidityChecker::registerAtom ( const Expr & e )

virtual

Register an atomic formula of interest.

Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function

virtual void CVC3::ValidityChecker::reprocessFlags ( )

virtual

Force reprocessing of all flags.

virtual void CVC3::ValidityChecker::reset ( )

virtual

Destroy and recreate validity checker: resets everything except for flags.

virtual QueryResult CVC3::ValidityChecker::restart ( const Expr & e )

virtual

Restart the most recent query with e as an additional assertion.

This method should only be called after a query which returns INVALID. Its return values are as for query().

virtual void CVC3::ValidityChecker::returnFromCheck ( )

virtual

Returns to context immediately before last invalid query.

This method should only be called after a query which returns false.

virtual int CVC3::ValidityChecker::scopeLevel ( )

virtual

Returns the current scope level. Initially, the scope level is 1.

virtual void CVC3::ValidityChecker::setMultiTrigger	(	const Expr &	e,
		const std::vector< Expr > &	multiTrigger
	)

virtual

Set a single multi-trigger for quantifier instantiation.

virtual void CVC3::ValidityChecker::setResourceLimit ( unsigned limit )

virtual

Set the resource limit (0==unlimited, 1==exhausted).

Currently, the limit is the total number of processed facts.

virtual void CVC3::ValidityChecker::setTimeLimit ( unsigned limit )

virtual

Set a time limit in tenth of a second,.

counting the cpu time used by the current process from now on. Currently, when the limit is reached, cvc3 tries to quickly terminate, probably with the status unknown.

virtual void CVC3::ValidityChecker::setTrigger	(	const Expr &	e,
		const Expr &	trigger
	)

virtual

Set a single trigger for quantifier instantiation.

virtual void CVC3::ValidityChecker::setTriggers	(	const Expr &	e,
		const std::vector< std::vector< Expr > > &	triggers
	)

virtual

Set triggers for quantifier instantiation.

Parameters

e	the expression for which triggers are being set.
triggers	Each item in triggers is a vector of Expr containing one or more patterns. A pattern is a term or Atomic predicate sub-expression of e. A vector containing more than one pattern is treated as a multi-trigger. Patterns will be matched in the order they occur in the vector.

virtual void CVC3::ValidityChecker::setTriggers	(	const Expr &	e,
		const std::vector< Expr > &	triggers
	)

virtual

Set triggers for quantifier instantiation (no multi-triggers)

virtual Expr CVC3::ValidityChecker::simplify ( const Expr & e )

virtual

Simplify e with respect to the current context.

virtual Expr CVC3::ValidityChecker::simulateExpr	(	const Expr &	f,
		const Expr &	s0,
		const std::vector< Expr > &	inputs,
		const Expr &	n
	)

virtual

Symbolic simulation expression.

Parameters

f	is the next state function (LAMBDA-expression)
s0	is the initial state
inputs	is the vector of LAMBDA-expressions representing the sequences of inputs to f
n	is a constant, the number of cycles to run the simulation.

virtual int CVC3::ValidityChecker::stackLevel ( )

virtual

Returns the current stack level. Initial level is 0.

virtual Expr CVC3::ValidityChecker::stringExpr ( const std::string & str )

virtual

Create a string Expr.

virtual Type CVC3::ValidityChecker::subrangeType	(	const Expr &	l,
		const Expr &	r
	)

virtual

Create a subrange type [l..r].

l and r can be Null; l=Null represents minus infinity, r=Null is plus infinity.

virtual Type CVC3::ValidityChecker::subtypeType	(	const Expr &	pred,
		const Expr &	witness
	)

virtual

Creates a subtype defined by the given predicate.

Parameters

pred	is a predicate taking one argument of type T and returning Boolean. The resulting type is a subtype of T whose elements x are those satisfying the predicate pred(x).
witness	is an expression of type T for which pred holds (if a Null expression is passed as a witness, cvc will try to prove $\exists x. pred(x))$ . if the witness check fails, a TypecheckException is thrown.

virtual Op CVC3::ValidityChecker::transClosure ( const Op & op )

virtual

Transitive closure of a binary predicate.

virtual Expr CVC3::ValidityChecker::trueExpr ( )

virtual

Return TRUE Expr.

virtual QueryResult CVC3::ValidityChecker::tryModelGeneration ( )

virtual

If the result of the last query was UNKNOWN try to actually build the model to verify the result.

This function should only be called after a query which return unknown.

virtual Expr CVC3::ValidityChecker::tupleExpr ( const std::vector< Expr > & exprs )

virtual

Tuple expression.

virtual Expr CVC3::ValidityChecker::tupleSelectExpr	(	const Expr &	tuple,
		int	index
	)

virtual

Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)

virtual Type CVC3::ValidityChecker::tupleType	(	const Type &	type0,
		const Type &	type1
	)

virtual

2-element tuple

virtual Type CVC3::ValidityChecker::tupleType	(	const Type &	type0,
		const Type &	type1,
		const Type &	type2
	)

virtual

3-element tuple

virtual Type CVC3::ValidityChecker::tupleType ( const std::vector< Type > & types )

virtual

n-element tuple (from a vector of types)

virtual Expr CVC3::ValidityChecker::tupleUpdateExpr	(	const Expr &	tuple,
		int	index,
		const Expr &	newValue
	)

virtual

Tuple update; equivalent to "tuple WITH index := newValue".

virtual Expr CVC3::ValidityChecker::uminusExpr ( const Expr & child )

virtual

Unary minus.

virtual FormulaValue CVC3::ValidityChecker::value ( const Expr & e )

virtual

virtual Expr CVC3::ValidityChecker::varExpr	(	const std::string &	name,
		const Type &	type
	)

virtual

Create a variable with a given name and type.

Parameters

name	is the name of the variable
type	is its type. The type cannot be a function type.

Returns: an Expr representation of a new variable

virtual Expr CVC3::ValidityChecker::varExpr	(	const std::string &	name,
		const Type &	type,
		const Expr &	def
	)

virtual

Create a variable with a given name, type, and value.

virtual Expr CVC3::ValidityChecker::writeExpr	(	const Expr &	array,
		const Expr &	index,
		const Expr &	newValue
	)

virtual

Array update; equivalent to "array WITH index := newValue".

Friends And Related Function Documentation

friend class Type

friend

Definition at line 526 of file cvc3_compat.h.

The documentation for this class was generated from the following file:

src/compat/cvc3_compat.h

Public Member Functions

Static Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation