45 TheoryRecords::rewriteAux(
const Expr& e) {
52 vector<unsigned> changed;
54 for(
int i=0, iend=e.
arity(); i<iend; ++i) {
62 res = substitutivityRule(e, changed, thms);
67 res = reflexivityRule(e);
72 thms.push_back(rewriteAux(e[0]));
73 if(thms[0].getLHS() != thms[0].getRHS()) {
74 res = substitutivityRule(
NOT, thms);
79 res = reflexivityRule(e);
91 TheoryRecords::rewriteAux(
const Theorem& thm) {
92 return iffMP(thm, rewriteAux(thm.
getExpr()));
118 kinds.push_back(
TUPLE);
141 TRACE(
"records",
"assertFact: enqueuing: ", expanded.
toString(),
"");
148 "expecting a disequality or boolean field extraction: "
152 DebugAssert(
false,
"TheoryRecords::assertFact expected an equation"
153 " or negation of equation expression. Instead it got"
163 TRACE(
"records",
"rewrite(", e,
") {");
164 bool needRecursion=
false;
168 switch(e[0].getOpKind()){
196 "TheoryRecords::rewrite(RECORD_UPDATE): e="+e.
toString());
197 if(e[0].getOpKind() ==
RECORD)
204 if(e[0].getOpKind() ==
TUPLE)
223 TRACE(
"records",
"rewrite => ", res.
getRHS(),
" }");
230 TRACE(
"records",
"computeTCC( ", e,
") {");
240 const std::string field(
getField(e));
254 DebugAssert (
false,
"Theory records cannot calculate this tcc");
257 TRACE(
"records",
"computeTCC => ", tcc,
"}");
265 const vector<Expr>& fields =
getFields(tExpr);
266 for(
unsigned int i = 0; i < fields.size() ; i++) {
273 for(
int i=0; i<tExpr.
arity(); i++) {
284 vector<Theorem> thms;
285 vector<unsigned> changed;
297 int size(lit.
arity());
298 for(
int i = 0; i < size ; i++) {
302 changed.push_back(i);
314 TRACE(
"typePred",
"ComputeTypePred[Records]", e,
"");
318 const vector<Expr>& fields =
getFields(tExpr);
319 vector<Expr> fieldPreds;
320 for(
unsigned int i = 0; i<fields.size(); i++) {
325 TRACE(
"typePred",
"Computed predicate ", pred,
"");
329 std::vector<Expr> fieldPreds;
330 for(
int i = 0; i<tExpr.
arity(); i++) {
334 TRACE(
"typePred",
"Computed predicate ", pred,
"");
338 DebugAssert(
false,
"computeTypePred[TheoryRecords] called with wrong type");
349 for (; i != iend; ) {
353 (
"Records cannot contain BOOLEANs: "
356 (
"Records cannot contain functions");
362 for (; i != iend; ) {
366 (
"Tuples cannot contain BOOLEANs: "
369 (
"Tuples cannot contain functions");
374 DebugAssert(
false,
"Unexpected kind in TheoryRecords::checkType"
382 bool enumerate,
bool computeSize)
393 vector<Expr> fieldTypes;
394 const vector<Expr>& fields =
getFields(e);
397 "size of fields does not match size of values");
398 for(
int i = 0; i<e.
arity(); ++i) {
400 "a record cannot not contain repeated fields"
402 fieldTypes.push_back(e[i].getType().getExpr());
403 previous=fields[i].getString();
413 "first child not a RECORD_TYPE" + e.
toString());
426 "first child not a RECORD_TYPE" + e.
toString());
430 (
"record update field \""+field
431 +
"\" does not match any in record type:\n"
432 +t.toString()+
"\n\nThe complete expression is:\n\n"
441 std::vector<Expr> types;
444 types.push_back((*it).getType().getExpr());
454 "incorrect TUPLE_SELECT expression: "
455 "first child is not a TUPLE_TYPE:\n\n" + e.
toString());
456 if(index >= t.arity())
467 "first child not a TUPLE_TYPE:\n\n" + e.
toString());
468 if(index >= t.arity())
500 "TheoryRecords::computeBaseType("+t.
toString()+
")");
518 i->addToNotify(
this, e);
528 TRACE(
"records",
"setup: lit = ", lit,
"");
530 vector<Theorem> thms;
531 vector<unsigned> changed;
532 for(
int i=0,iend=lit.arity(); i<iend; ++i) {
537 if(lit[i] != t.
getRHS()) {
539 changed.push_back(i);
542 if(changed.size()>0) {
574 if (
find(d).getRHS() == d) {
590 int i=0, iend=e.
arity();
592 if(i!=iend) os << e[i];
594 for(; i!=iend; ++i) os << push <<
"," <<
pop <<
space << e[i];
599 int i=0, iend=e.
arity();
601 if(i!=iend) os << e[i];
603 for(; i!=iend; ++i) os << push <<
"," <<
pop <<
space << e[i];
608 size_t i=0, iend=e.
arity();
613 const vector<Expr>& fields =
getFields(e);
614 if(iend != fields.size()) {
620 os << fields[i].getString() <<
space
621 <<
":="<<
space << push << e[i] <<
pop;
625 os << push <<
"," <<
pop <<
space << fields[i].getString()
627 <<
":="<<
space << push << e[i] <<
pop;
628 os << push <<
space <<
"#)";
632 size_t i=0, iend=e.
arity();
637 const vector<Expr>& fields =
getFields(e);
638 if(iend != fields.size()) {
644 os << fields[i].getString() <<
":"<<
space << push << e[i] <<
pop;
648 os << push <<
"," <<
pop <<
space << fields[i].getString()
649 <<
":"<<
space << push << e[i] <<
pop;
650 os << push <<
space <<
"#]";
669 os <<
"(" <<
push << e[0] <<
space <<
"WITH ."
677 os <<
"(" << push << e[0] <<
space <<
"WITH ."
679 <<
space <<
":=" <<
space << push << e[1] << push <<
")";
695 int i=0, iend=e.
arity();
696 os <<
"(" <<
push <<
"TUPLE";
697 for(; i<iend; ++i) os <<
space << e[i];
702 int i=0, iend=e.
arity();
703 os <<
"(" <<
push <<
"TUPLE_TYPE";
704 for(; i!=iend; ++i) os <<
space << e[i];
709 size_t i=0, iend=e.
arity();
714 const vector<Expr>& fields =
getFields(e);
715 if(iend != fields.size()) {
719 os <<
"(" <<
push <<
"RECORD";
721 os <<
space <<
"(" << push << fields[i].getString() <<
space
722 << e[i] << push <<
")" <<
pop <<
pop;
727 size_t i=0, iend=e.
arity();
732 const vector<Expr>& fields =
getFields(e);
733 if(iend != fields.size()) {
737 os <<
"(" <<
push <<
"RECORD_TYPE";
739 os <<
space <<
"(" << push << fields[i].getString()
741 os << push <<
space <<
")";
746 os <<
"(" <<
push <<
"RECORD_SELECT" <<
space
753 os <<
"(" << push <<
"TUPLE_SELECT" <<
space
760 os <<
"(" << push <<
"RECORD_UPDATE" <<
space
762 <<
space << e[1] << push <<
")";
768 os <<
"(" << push <<
"TUPLE_UPDATE" <<
space << e[0]
770 <<
space << e[1] << push <<
")";
783 int i=0, iend=e.
arity();
784 os <<
"(" <<
push <<
"TUPLE";
785 for(; i<iend; ++i) os <<
space << e[i];
790 int i=0, iend=e.
arity();
791 os <<
"(" <<
push <<
"TUPLE_TYPE";
792 for(; i!=iend; ++i) os <<
space << e[i];
797 size_t i=0, iend=e.
arity();
802 const vector<Expr>& fields =
getFields(e);
803 if(iend != fields.size()) {
807 os <<
"(" <<
push <<
"RECORD";
809 os <<
space <<
"(" << push << fields[i].getString() <<
space
810 << e[i] << push <<
")" <<
pop <<
pop;
815 size_t i=0, iend=e.
arity();
820 const vector<Expr>& fields =
getFields(e);
821 if(iend != fields.size()) {
825 os <<
"(" <<
push <<
"RECORD_TYPE";
827 os <<
space <<
"(" << push << fields[i].getString()
829 os << push <<
space <<
")";
834 os <<
"(" <<
push <<
"RECORD_SELECT" <<
space
841 os <<
"(" << push <<
"TUPLE_SELECT" <<
space
848 os <<
"(" << push <<
"RECORD_UPDATE" <<
space
850 <<
space << e[1] << push <<
")";
856 os <<
"(" << push <<
"TUPLE_UPDATE" <<
space << e[0]
858 <<
space << e[1] << push <<
")";
881 TRACE(
"parser",
"TheoryRecords::parseExprOp(", e,
")");
887 "TheoryRecords::parseExprOp:\n e = "+e.
toString());
889 const Expr& c1 = e[0][0];
901 for(; i!=iend; ++i) {
902 if(i->
arity() != 2 || (*i)[0].getKind() !=
ID)
905 fields.push_back((*i)[0][0]);
952 "TheoryRecords::parseExprOp: invalid command or expression: " + e.
toString());
962 const std::vector<Expr>& kids) {
963 vector<Expr> fieldExprs;
964 vector<string>::const_iterator i = fields.begin(), iend = fields.end();
965 for (; i != iend; ++i) fieldExprs.push_back(
getEM()->newStringExpr(*i));
971 const std::vector<Expr>& kids) {
978 const std::vector<Type>& types) {
980 for(vector<Type>::const_iterator i=types.begin(), iend=types.end();
982 kids.push_back(i->getExpr());
989 const std::vector<Expr>& types) {
990 vector<Expr> fieldExprs;
991 vector<string>::const_iterator i = fields.begin(), iend = fields.end();
992 for (; i != iend; ++i) fieldExprs.push_back(
getEM()->newStringExpr(*i));
998 const std::vector<Expr>& types) {
1020 "TheoryRecords::getFields: Not a record literal: "
1030 "TheoryRecords::getField: Not a record literal: "
1038 const vector<Expr>& fields =
getFields(e);
1039 for(
size_t i=0, iend=fields.size(); i<iend; ++i) {
1040 if(fields[i].getString() == field)
return i;
1043 +
", field="+field+
"): field is not found");
1052 "TheoryRecords::getField: Not a record literal: ");
1066 for(vector<Type>::const_iterator i=types.begin(), iend=types.end();
1068 kids.push_back(i->getExpr());
1095 "TheoryRecords::getField: Not a record literal: ");
virtual Expr parseExpr(const Expr &e)
Parse the generic expression.
ExprStream & pop(ExprStream &os)
Restore the indentation.
void setupTerm(const Expr &e, Theory *i, const Theorem &thm)
Setup additional terms within a theory-specific setup().
iterator begin() const
Begin iterator.
ExprStream & printAST(ExprStream &os) const
Print the top node and then recurse through the children */.
TheoryCore * theoryCore()
Get a pointer to theoryCore.
Data structure of expressions in CVC3.
const Theorem & getFind() const
ExprManager * getEM() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Type recordType(const std::vector< std::string > &fields, const std::vector< Type > &types)
Create a record type.
An exception thrown by the parser.
virtual void assertEqualities(const Theorem &e)
Handle new equalities (usually asserted through addFact)
void setupCC(const Expr &e)
Setup a term for congruence closure (must have sig and rep attributes)
virtual Theorem expandEq(const Theorem &eqThrm)=0
From T|- e = e' return T|- AND (e.i = e'.i) for all i.
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
An exception to be thrown at typecheck error.
Expr tupleSelect(const Expr &tup, int i)
Create a tuple index selector expression.
bool isRecordAccess(const Expr &e)
Test whether expr is a record select/update subclass.
bool isRecordType(const Expr &e)
Test whether expr is a record type.
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
MS C++ specific settings.
void checkType(const Expr &e)
check record or tuple type
virtual void enqueueFact(const Theorem &e)
Submit a derived fact to the core from a decision procedure.
Lisp-like format for automatically generated specs.
ExprStream & space(ExprStream &os)
Insert a single white space separator.
Theorem rewriteAnd(const Expr &e)
==> AND(e1,e2) IFF [simplified expr]
#define DebugAssert(cond, str)
virtual Theorem rewriteLitSelect(const Expr &e)=0
==> (REC_LITERAL (f1 v1) ... (fi vi) ...).fi = vi
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
const std::vector< Expr > & getKids() const
RecordsProofRules * d_rules
void registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new theory.
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Op getOp() const
Get operator from expression.
const Expr & getExpr() const
virtual void assignValue(const Expr &t, const Expr &val)
Assigns t a concrete value val. Used in model generation.
virtual Theorem expandRecord(const Expr &e)=0
Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #)
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Expr recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &kids)
Create a record literal.
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
virtual Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Identifier is (ID (STRING_EXPR "name"))
std::string toString() const
Theorem rewriteCC(const Expr &e)
Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
void computeType(const Expr &e)
computes the type of a record or a tuple
std::string toString() const
Print the expression to a string.
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
std::string int2string(int n)
const Expr & getRHS() const
Theorem getModelValue(const Expr &e)
Fetch the concrete assignment to the variable during model generation.
Theorem rewrite(const Expr &e)
rewrites an expression e to one of several allowed forms
Expr getTypePred(const Type &t, const Expr &e)
Calls the correct theory to compute a type predicate.
std::string toString() const
void assertFact(const Theorem &e)
assert a fact to the theory of records
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
ExprManager * getEM()
Access to ExprManager.
Type tupleType(const std::vector< Type > &types)
Create a tuple type.
bool isRecord(const Expr &e)
Test whether expr is a record literal.
const std::string & getName() const
RecordsProofRules * createProofRules()
creates a reference to the proof rules
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Theorem rewriteAux(const Expr &e)
Auxiliary rewrites: Processing of AND and OR of equations. Returns e=e'.
Theorem updateHelper(const Expr &e)
Update the children of the term e.
void setType(const Type &t) const
Set the cached type.
Type getBaseType(const Expr &e)
Compute (or look up in cache) the base type of e and return the result.
void updateCC(const Theorem &e, const Expr &d)
Update a term w.r.t. congruence closure (must be setup with setupCC())
virtual bool inconsistent()
Check if the current context is inconsistent.
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
Expr recordUpdate(const Expr &r, const std::string &field, const Expr &val)
Create a record field update expression.
An exception to be thrown by the smtlib translator.
virtual Theorem rewriteUpdateSelect(const Expr &e)=0
==> (REC_SELECT (REC_UPDATE e fi vi) fi) = vi
bool isTupleAccess(const Expr &e)
Test whether expr is a tuple select/update subclass.
ExprStream & print(ExprStream &os, const Expr &e)
pretty printing
int getFieldIndex(const Expr &e, const std::string &field)
Get the field index in the record literal or type.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
const Expr & getLHS() const
bool isTupleType(const Expr &e)
Test if expr represents a tuple type.
Expr tupleUpdate(const Expr &tup, int i, const Expr &val)
Create a tuple index update expression.
Theorem reflexivityRule(const Expr &a)
==> a == a
Theorem substitutivityRule(const Op &op, const std::vector< Theorem > &thms)
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Cardinality
Enum for cardinality of types.
const std::string & getString() const
Type getType() const
Get the type. Recursively compute if necessary.
virtual Theorem expandTuple(const Expr &e)=0
Expand a tuple into a literal: |- e = (e.0, ..., e.n-1)
InputLanguage lang() const
Get the current output language.
const std::vector< Expr > & getFields(const Expr &r)
Get the list of fields from a record literal.
Expr andExpr(const std::vector< Expr > &children)
Theorem find(const Expr &e)
Return the theorem that e is equal to its find.
virtual Theorem rewriteLitUpdate(const Expr &e)=0
==> (REC_UPDATE (REC_LITERAL (f1 v1) ... (fi vi) ...) fi v') =(REC_LITERAL (f1 v1) ...
int getIndex(const Expr &e)
Get the index from the tuple select and update expressions.
const std::string & getField(const Expr &e, int i)
Get the i-th field name from the record literal or type.
Expr recordSelect(const Expr &r, const std::string &field)
Create a record field select expression.
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Theorem symmetryRule(const Theorem &a1_eq_a2)
a1 == a2 ==> a2 == a1
Nice SAL-like language for manually written specs.
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
Expr tupleExpr(const std::vector< Expr > &kids)
Create a tuple literal.
iterator end() const
End iterator.