* to add typing rules to theory_$dir_type_rules.h for your operators
and constants
* to write code in theory_$dir_rewriter.h to implement a normal form
- for your theory's terms
+ for your theory's terms; in particular, you should ensure that you
+ rewrite (= X X) to "true" for terms X of your theory's sorts, and
+ evaluate any constant terms
* for any new types that you have introduced, add "mk*Type()" functions to
the NodeManager and ExprManager in src/expr/node_manager.{h,cpp} and
src/expr/expr_manager_template.{h,cpp}. You may also want "is*()" testers
theory/unconstrained_simplifier.cpp \
theory/quantifiers_engine.h \
theory/quantifiers_engine.cpp \
- theory/model.h \
- theory/model.cpp \
+ theory/theory_model.h \
+ theory/theory_model.cpp \
theory/rep_set.h \
theory/rep_set.cpp \
theory/atom_requests.h \
#include "util/output.h"
#include "util/dump.h"
#include "util/sexpr.h"
-#include "util/util_model.h"
+#include "util/model.h"
#include "expr/node.h"
#include "printer/printer.h"
case kind::BUILTIN:
typeNode = nodeManager->builtinOperatorType();
break;
- case kind::BITVECTOR_EXTRACT_OP :
- typeNode = nodeManager->builtinOperatorType();
- break;
${typerules}
-#line 50 "${template}"
+#line 47 "${template}"
default:
Debug("getType") << "FAILURE" << std::endl;
switch(n.getKind()) {
${construles}
-#line 73 "${template}"
+#line 70 "${template}"
default:;
}
#include "theory/substitutions.h"
#include "smt/smt_engine.h"
#include "smt/options.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/arrays/theory_arrays_rewriter.h"
#include "printer/dagification_visitor.h"
#include "util/node_visitor.h"
#include "util/language.h"
#include "util/sexpr.h"
-#include "util/util_model.h"
+#include "util/model.h"
#include "expr/node.h"
#include "expr/command.h"
#include "smt/options.h"
#include "expr/node_manager_attributes.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/arrays/theory_arrays_rewriter.h"
using namespace std;
#include "smt/boolean_terms.h"
#include "smt/smt_engine.h"
#include "theory/theory_engine.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/booleans/boolean_term_conversion_mode.h"
#include "theory/booleans/options.h"
#include "expr/kind.h"
#include "theory/booleans/boolean_term_conversion_mode.h"
#include "theory/booleans/options.h"
#include "util/ite_removal.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "printer/printer.h"
#include "prop/options.h"
#include "theory/arrays/options.h"
return false;
}
- // No, conflict, go through the literals and solve them
+ // No conflict, go through the literals and solve them
SubstitutionMap constantPropagations(d_smt.d_context);
SubstitutionMap newSubstitutions(d_smt.d_context);
SubstitutionMap::iterator pos;
Assert(d_topLevelSubstitutions.apply(t) == t);
Assert(newSubstitutions.apply(t) == t);
constantPropagations.addSubstitution(t, c);
- // vector<pair<Node,Node> > equations;a
+ // vector<pair<Node,Node> > equations;
// constantPropagations.simplifyLHS(t, c, equations, true);
// if (!equations.empty()) {
// Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
// }
Assert(constantPropagations.apply((*pos).second) == (*pos).second);
}
-#endif
+#endif /* CVC4_ASSERTIONS */
}
// Resize the learnt
d_nonClausalLearnedLiterals.resize(j);
#include "theory/arith/constraint.h"
#include "theory/arith/theory_arith.h"
#include "theory/arith/normal_form.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/arith/options.h"
#include "theory/arith/constraint.h"
#include "theory/arith/theory_arith.h"
#include "theory/arith/normal_form.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/arith/options.h"
if( check ) {
TypeNode lhsType = n[0].getType(check);
if (!lhsType.isReal()) {
- Message() << lhsType << " : " << n[0] << std::endl;
throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side");
}
TypeNode rhsType = n[1].getType(check);
#include <map>
#include "theory/rewriter.h"
#include "expr/command.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/arrays/options.h"
#include "smt/logic_exception.h"
+/********************* */
+/*! \file atom_requests.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
#include "theory/atom_requests.h"
using namespace CVC4;
+/********************* */
+/*! \file atom_requests.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
#pragma once
#include "expr/node.h"
return PP_ASSERT_STATUS_CONFLICT;
}
- // Add the substitution from the variable to it's value
+ // Add the substitution from the variable to its value
if (in.getKind() == kind::NOT) {
if (in[0].getKind() == kind::VARIABLE) {
outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false));
if ((*i).getKind() == kind::OR) done = false;
}
if (!done) {
- return flattenNode(n, /*trivialNode = */ tt, /* skipNode = */ ff);
+ return flattenNode(n, /* trivialNode = */ tt, /* skipNode = */ ff);
}
break;
}
if ((*i).getKind() == kind::AND) done = false;
}
if (!done) {
- RewriteResponse ret = flattenNode(n, /*trivialNode = */ ff, /* skipNode = */ tt);
+ RewriteResponse ret = flattenNode(n, /* trivialNode = */ ff, /* skipNode = */ tt);
Debug("bool-flatten") << n << ": " << ret.node << std::endl;
return ret;
}
#include "theory/builtin/theory_builtin.h"
#include "theory/valuation.h"
#include "expr/kind.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
using namespace std;
#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/options.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
using namespace std;
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/bv/slicer.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/bv/options.h"
using namespace std;
#include "theory/bv/bv_subtheory_inequality.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
using namespace std;
using namespace CVC4;
typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule
typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule
#include "theory/bv/bv_subtheory_core.h"
#include "theory/bv/bv_subtheory_inequality.h"
#include "theory/bv/bv_subtheory_bitblast.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
using namespace CVC4;
using namespace CVC4::theory;
}
};
+class BitVectorExtractOpTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP);
+ return nodeManager->builtinOperatorType();
+ }
+};
+
class BitVectorConcatRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
#include "util/cvc4_assert.h"
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/theory_datatypes_type_rules.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "smt/options.h"
#include "smt/boolean_terms.h"
#include "theory/quantifiers/options.h"
}else{
return NodeManager::currentNM()->mkNode( AND, assumptions );
}
-}
\ No newline at end of file
+}
** Rewriter attributes.
**/
-#ifndef __CVC4__THEORY__DECISION_ATRRIBUTES
-#define __CVC4__THEORY__DECISION_ATRRIBUTES
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__DECISION_ATTRIBUTES
+#define __CVC4__THEORY__DECISION_ATTRIBUTES
#include "expr/attribute.h"
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__DECISION_ATRRIBUTES */
+#endif /* __CVC4__THEORY__DECISION_ATTRIBUTES */
+++ /dev/null
-/********************* */
-/*! \file model.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters, Clark Barrett
- ** Minor contributors (to current version): Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of model class
- **/
-
-#include "theory/model.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/type_enumerator.h"
-#include "smt/options.h"
-#include "smt/smt_engine.h"
-#include "theory/uf/theory_uf_model.h"
-#include "theory/uf/options.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-
-TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) :
- d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
-{
- d_true = NodeManager::currentNM()->mkConst( true );
- d_false = NodeManager::currentNM()->mkConst( false );
-
- d_eeContext = new context::Context();
- d_equalityEngine = new eq::EqualityEngine(d_eeContext, name);
-
- // The kinds we are treating as function application in congruence
- d_equalityEngine->addFunctionKind(kind::APPLY_UF);
- d_equalityEngine->addFunctionKind(kind::SELECT);
- // d_equalityEngine->addFunctionKind(kind::STORE);
- d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
- d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
- d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
- d_eeContext->push();
-}
-
-void TheoryModel::reset(){
- d_reps.clear();
- d_rep_set.clear();
- d_uf_terms.clear();
- d_uf_models.clear();
- d_eeContext->pop();
- d_eeContext->push();
-}
-
-Node TheoryModel::getValue(TNode n) const {
- //apply substitutions
- Node nn = d_substitutions.apply(n);
- //get value in model
- nn = getModelValue(nn);
- if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
- //normalize
- nn = Rewriter::rewrite(nn);
- }
- return nn;
-}
-
-Expr TheoryModel::getValue( Expr expr ) const{
- Node n = Node::fromExpr( expr );
- Node ret = getValue( n );
- return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr();
-}
-
-/** get cardinality for sort */
-Cardinality TheoryModel::getCardinality( Type t ) const{
- TypeNode tn = TypeNode::fromType( t );
- //for now, we only handle cardinalities for uninterpreted sorts
- if( tn.isSort() ){
- if( d_rep_set.hasType( tn ) ){
- return Cardinality( d_rep_set.getNumRepresentatives( tn ) );
- }else{
- return Cardinality( CardinalityUnknown() );
- }
- }else{
- return Cardinality( CardinalityUnknown() );
- }
-}
-
-Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
-{
- if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL) {
- // We should have terms, thanks to TheoryQuantifiers::collectModelInfo().
- // However, if the Decision Engine stops us early, there might be a
- // quantifier that isn't assigned. In conjunction with miniscoping, this
- // might lead to a perfectly good model. Think of
- // ASSERT FORALL(x) : p OR x=5
- // The p is pulled out by miniscoping, and set to TRUE by the decision
- // engine, then the quantifier's value in the model doesn't matter, so the
- // Decision Engine stops. So even though the top-level quantifier was
- // asserted, it can't be checked directly: first, it doesn't "exist" in
- // non-miniscoped form, and second, no quantifiers have been asserted, so
- // none is in the model. We used to fail an assertion here, but that's
- // no good. Instead, return the quantifier itself. If we're in
- // checkModel(), and the quantifier actually matters, we'll get an
- // assert-fail since the quantifier isn't a constant.
- if(!d_equalityEngine->hasTerm(Rewriter::rewrite(n))) {
- return n;
- } else {
- n = Rewriter::rewrite(n);
- }
- } else {
- if(n.getKind() == kind::LAMBDA) {
- NodeManager* nm = NodeManager::currentNM();
- Node body = getModelValue(n[1], true);
- body = Rewriter::rewrite(body);
- return nm->mkNode(kind::LAMBDA, n[0], body);
- }
- if(n.isConst() || (hasBoundVars && n.getKind() == kind::BOUND_VARIABLE)) {
- return n;
- }
-
- TypeNode t = n.getType();
- if (t.isFunction() || t.isPredicate()) {
- if (d_enableFuncModels) {
- std::map< Node, Node >::const_iterator it = d_uf_models.find(n);
- if (it != d_uf_models.end()) {
- // Existing function
- return it->second;
- }
- // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
- vector<TypeNode> argTypes = t.getArgTypes();
- vector<Node> args;
- NodeManager* nm = NodeManager::currentNM();
- for (unsigned i = 0; i < argTypes.size(); ++i) {
- args.push_back(nm->mkBoundVar(argTypes[i]));
- }
- Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
- TypeEnumerator te(t.getRangeType());
- return nm->mkNode(kind::LAMBDA, boundVarList, *te);
- }
- // TODO: if func models not enabled, throw an error?
- Unreachable();
- }
-
- if (n.getNumChildren() > 0) {
- std::vector<Node> children;
- if (n.getKind() == APPLY_UF) {
- Node op = getModelValue(n.getOperator(), hasBoundVars);
- children.push_back(op);
- }
- else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
- children.push_back(n.getOperator());
- }
- //evaluate the children
- for (unsigned i = 0; i < n.getNumChildren(); ++i) {
- Node val = getModelValue(n[i], hasBoundVars);
- children.push_back(val);
- }
- Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));
- if(val.getKind() == kind::CARDINALITY_CONSTRAINT) {
- val = NodeManager::currentNM()->mkConst(getCardinality(val[0].getType().toType()).getFiniteCardinality() <= val[1].getConst<Rational>().getNumerator());
- }
- if(val.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){
- //FIXME
- val = NodeManager::currentNM()->mkConst(false);
- }
- return val;
- }
-
- if (!d_equalityEngine->hasTerm(n)) {
- // Unknown term - return first enumerated value for this type
- TypeEnumerator te(n.getType());
- return *te;
- }
- }
- Node val = d_equalityEngine->getRepresentative(n);
- Assert(d_reps.find(val) != d_reps.end());
- std::map< Node, Node >::const_iterator it = d_reps.find( val );
- if( it!=d_reps.end() ){
- return it->second;
- }else{
- return Node::null();
- }
-}
-
-Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
- if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){
- //try to find a pre-existing arbitrary element
- for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){
- if( std::find( exclude.begin(), exclude.end(), d_rep_set.d_type_reps[tn][i] )==exclude.end() ){
- return d_rep_set.d_type_reps[tn][i];
- }
- }
- }
- return Node::null();
-}
-
-//FIXME: need to ensure that theory enumerators exist for each sort
-Node TheoryModel::getNewDomainValue( TypeNode tn ){
- if( tn.isSort() ){
- return Node::null();
- }else{
- TypeEnumerator te(tn);
- while( !te.isFinished() ){
- Node r = *te;
- if(Debug.isOn("getNewDomainValue")) {
- Debug("getNewDomainValue") << "getNewDomainValue( " << tn << ")" << endl;
- Debug("getNewDomainValue") << "+ TypeEnumerator gave: " << r << endl;
- Debug("getNewDomainValue") << "+ d_type_reps are:";
- for(vector<Node>::const_iterator i = d_rep_set.d_type_reps[tn].begin();
- i != d_rep_set.d_type_reps[tn].end();
- ++i) {
- Debug("getNewDomainValue") << " " << *i;
- }
- Debug("getNewDomainValue") << endl;
- }
- if( std::find(d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r) ==d_rep_set.d_type_reps[tn].end() ) {
- Debug("getNewDomainValue") << "+ it's new, so returning " << r << endl;
- return r;
- }
- ++te;
- }
- return Node::null();
- }
-}
-
-/** add substitution */
-void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
- if( !d_substitutions.hasSubstitution( x ) ){
- d_substitutions.addSubstitution( x, t, invalidateCache );
- } else {
-#ifdef CVC4_ASSERTIONS
- Node oldX = d_substitutions.getSubstitution(x);
- // check that either the old substitution is the same, or it now maps to the new substitution
- if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) {
- stringstream ss;
- ss << "Two incompatible substitutions added to TheoryModel:\n"
- << "the term: " << x << "\n"
- << "old mapping: " << d_substitutions.apply(oldX) << "\n"
- << "new mapping: " << d_substitutions.apply(t);
- InternalError(ss.str());
- }
-#endif /* CVC4_ASSERTIONS */
- }
-}
-
-/** add term */
-void TheoryModel::addTerm(TNode n ){
- Assert(d_equalityEngine->hasTerm(n));
- //must collect UF terms
- if (n.getKind()==APPLY_UF) {
- Node op = n.getOperator();
- if( std::find( d_uf_terms[ op ].begin(), d_uf_terms[ op ].end(), n )==d_uf_terms[ op ].end() ){
- d_uf_terms[ op ].push_back( n );
- Trace("model-add-term-uf") << "Add term " << n << std::endl;
- }
- }
-}
-
-/** assert equality */
-void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){
- if (a == b && polarity) {
- return;
- }
- Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl;
- d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() );
- Assert(d_equalityEngine->consistent());
-}
-
-/** assert predicate */
-void TheoryModel::assertPredicate(TNode a, bool polarity ){
- if ((a == d_true && polarity) ||
- (a == d_false && (!polarity))) {
- return;
- }
- if (a.getKind() == EQUAL) {
- Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl;
- d_equalityEngine->assertEquality( a, polarity, Node::null() );
- } else {
- Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl;
- d_equalityEngine->assertPredicate( a, polarity, Node::null() );
- Assert(d_equalityEngine->consistent());
- }
-}
-
-/** assert equality engine */
-void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* termSet)
-{
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
- for (; !eqcs_i.isFinished(); ++eqcs_i) {
- Node eqc = (*eqcs_i);
- bool predicate = false;
- bool predTrue = false;
- bool predFalse = false;
- if (eqc.getType().isBoolean()) {
- predicate = true;
- predTrue = ee->areEqual(eqc, d_true);
- predFalse = ee->areEqual(eqc, d_false);
- }
- eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
- bool first = true;
- Node rep;
- for (; !eqc_i.isFinished(); ++eqc_i) {
- if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) {
- continue;
- }
- if (predicate) {
- if (predTrue) {
- assertPredicate(*eqc_i, true);
- }
- else if (predFalse) {
- assertPredicate(*eqc_i, false);
- }
- else {
- if (first) {
- rep = (*eqc_i);
- first = false;
- }
- else {
- Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl;
- d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null());
- Assert(d_equalityEngine->consistent());
- }
- }
- } else {
- if (first) {
- rep = (*eqc_i);
- first = false;
- }
- else {
- assertEquality(*eqc_i, rep, true);
- }
- }
- }
- }
-}
-
-void TheoryModel::assertRepresentative(TNode n )
-{
- Trace("model-builder-reps") << "Assert rep : " << n << std::endl;
- d_reps[ n ] = n;
-}
-
-bool TheoryModel::hasTerm(TNode a)
-{
- return d_equalityEngine->hasTerm( a );
-}
-
-Node TheoryModel::getRepresentative(TNode a)
-{
- if( d_equalityEngine->hasTerm( a ) ){
- Node r = d_equalityEngine->getRepresentative( a );
- if( d_reps.find( r )!=d_reps.end() ){
- return d_reps[ r ];
- }else{
- return r;
- }
- }else{
- return a;
- }
-}
-
-bool TheoryModel::areEqual(TNode a, TNode b)
-{
- if( a==b ){
- return true;
- }else if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){
- return d_equalityEngine->areEqual( a, b );
- }else{
- return false;
- }
-}
-
-bool TheoryModel::areDisequal(TNode a, TNode b)
-{
- if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){
- return d_equalityEngine->areDisequal( a, b, false );
- }else{
- return false;
- }
-}
-
-//for debugging
-void TheoryModel::printRepresentativeDebug( const char* c, Node r ){
- if( r.isNull() ){
- Trace( c ) << "null";
- }else if( r.getType().isBoolean() ){
- if( areEqual( r, d_true ) ){
- Trace( c ) << "true";
- }else{
- Trace( c ) << "false";
- }
- }else{
- Trace( c ) << getRepresentative( r );
- }
-}
-
-void TheoryModel::printRepresentative( std::ostream& out, Node r ){
- Assert( !r.isNull() );
- if( r.isNull() ){
- out << "null";
- }else if( r.getType().isBoolean() ){
- if( areEqual( r, d_true ) ){
- out << "true";
- }else{
- out << "false";
- }
- }else{
- out << getRepresentative( r );
- }
-}
-
-
-TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){
-
-}
-
-
-bool TheoryEngineModelBuilder::isAssignable(TNode n)
-{
- return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR);
-}
-
-
-void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache)
-{
- if (n.getKind()==FORALL || n.getKind()==EXISTS) {
- return;
- }
- if (cache.find(n) != cache.end()) {
- return;
- }
- if (isAssignable(n)) {
- tm->d_equalityEngine->addTerm(n);
- }
- for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
- checkTerms(*child_it, tm, cache);
- }
- cache.insert(n);
-}
-
-
-void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
-{
- Trace("model-builder") << "TheoryEngineModelBuilder: buildModel, fullModel = " << fullModel << std::endl;
- TheoryModel* tm = (TheoryModel*)m;
-
- // buildModel with fullModel = true should only be called once in any context
- Assert(!tm->d_modelBuilt);
- tm->d_modelBuilt = fullModel;
-
- // Reset model
- tm->reset();
-
- // Collect model info from the theories
- Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
- d_te->collectModelInfo(tm, fullModel);
-
- // Loop through all terms and make sure that assignable sub-terms are in the equality engine
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine );
- {
- NodeSet cache;
- for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
- eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i),tm->d_equalityEngine);
- for ( ; !eqc_i.isFinished(); ++eqc_i) {
- checkTerms(*eqc_i, tm, cache);
- }
- }
- }
-
- Trace("model-builder") << "Collect representatives..." << std::endl;
-
- // Process all terms in the equality engine, store representatives for each EC
- std::map< Node, Node > assertedReps, constantReps;
- TypeSet typeConstSet, typeRepSet, typeNoRepSet;
- std::set< TypeNode > allTypes;
- eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
- for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
-
- // eqc is the equivalence class representative
- Node eqc = (*eqcs_i);
- Trace("model-builder") << "Processing EC: " << eqc << endl;
- Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
- TypeNode eqct = eqc.getType();
- Assert(assertedReps.find(eqc) == assertedReps.end());
- Assert(constantReps.find(eqc) == constantReps.end());
-
- // Loop through terms in this EC
- Node rep, const_rep;
- eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
- for ( ; !eqc_i.isFinished(); ++eqc_i) {
- Node n = *eqc_i;
- Trace("model-builder") << " Processing Term: " << n << endl;
- // Record as rep if this node was specified as a representative
- if (tm->d_reps.find(n) != tm->d_reps.end()){
- Assert(rep.isNull());
- rep = tm->d_reps[n];
- Assert(!rep.isNull() );
- Trace("model-builder") << " Rep( " << eqc << " ) = " << rep << std::endl;
- }
- // Record as const_rep if this node is constant
- if (n.isConst()) {
- Assert(const_rep.isNull());
- const_rep = n;
- Trace("model-builder") << " ConstRep( " << eqc << " ) = " << const_rep << std::endl;
- }
- //model-specific processing of the term
- tm->addTerm(n);
- }
-
- // Assign representative for this EC
- if (!const_rep.isNull()) {
- // Theories should not specify a rep if there is already a constant in the EC
- Assert(rep.isNull() || rep == const_rep);
- constantReps[eqc] = const_rep;
- typeConstSet.add(eqct.getBaseType(), const_rep);
- }
- else if (!rep.isNull()) {
- assertedReps[eqc] = rep;
- typeRepSet.add(eqct.getBaseType(), eqc);
- allTypes.insert(eqct);
- }
- else {
- typeNoRepSet.add(eqct, eqc);
- allTypes.insert(eqct);
- }
- }
-
- // Need to ensure that each EC has a constant representative.
-
- Trace("model-builder") << "Processing EC's..." << std::endl;
-
- TypeSet::iterator it;
- set<TypeNode>::iterator type_it;
- set<Node>::iterator i, i2;
- bool changed, unassignedAssignable, assignOne = false;
- set<TypeNode> evaluableSet;
-
- // Double-fixed-point loop
- // Outer loop handles a special corner case (see code at end of loop for details)
- for (;;) {
-
- // Inner fixed-point loop: we are trying to learn constant values for every EC. Each time through this loop, we process all of the
- // types by type and may learn some new EC values. EC's in one type may depend on EC's in another type, so we need a fixed-point loop
- // to ensure that we learn as many EC values as possible
- do {
- changed = false;
- unassignedAssignable = false;
- evaluableSet.clear();
-
- // Iterate over all types we've seen
- for (type_it = allTypes.begin(); type_it != allTypes.end(); ++type_it) {
- TypeNode t = *type_it;
- TypeNode tb = t.getBaseType();
- set<Node>* noRepSet = typeNoRepSet.getSet(t);
-
- // 1. Try to evaluate the EC's in this type
- if (noRepSet != NULL && !noRepSet->empty()) {
- Trace("model-builder") << " Eval phase, working on type: " << t << endl;
- bool assignable, evaluable, evaluated;
- d_normalizedCache.clear();
- for (i = noRepSet->begin(); i != noRepSet->end(); ) {
- i2 = i;
- ++i;
- assignable = false;
- evaluable = false;
- evaluated = false;
- eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine);
- for ( ; !eqc_i.isFinished(); ++eqc_i) {
- Node n = *eqc_i;
- if (isAssignable(n)) {
- assignable = true;
- }
- else {
- evaluable = true;
- Node normalized = normalize(tm, n, constantReps, true);
- if (normalized.isConst()) {
- typeConstSet.add(tb, normalized);
- constantReps[*i2] = normalized;
- Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
- changed = true;
- evaluated = true;
- noRepSet->erase(i2);
- break;
- }
- }
- }
- if (!evaluated) {
- if (evaluable) {
- evaluableSet.insert(tb);
- }
- if (assignable) {
- unassignedAssignable = true;
- }
- }
- }
- }
-
- // 2. Normalize any non-const representative terms for this type
- set<Node>* repSet = typeRepSet.getSet(t);
- if (repSet != NULL && !repSet->empty()) {
- Trace("model-builder") << " Normalization phase, working on type: " << t << endl;
- d_normalizedCache.clear();
- for (i = repSet->begin(); i != repSet->end(); ) {
- Assert(assertedReps.find(*i) != assertedReps.end());
- Node rep = assertedReps[*i];
- Node normalized = normalize(tm, rep, constantReps, false);
- Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
- if (normalized.isConst()) {
- changed = true;
- typeConstSet.add(t.getBaseType(), normalized);
- constantReps[*i] = normalized;
- assertedReps.erase(*i);
- i2 = i;
- ++i;
- repSet->erase(i2);
- }
- else {
- if (normalized != rep) {
- assertedReps[*i] = normalized;
- changed = true;
- }
- ++i;
- }
- }
- }
- }
- } while (changed);
-
- if (!fullModel || !unassignedAssignable) {
- break;
- }
-
- // 3. Assign unassigned assignable EC's using type enumeration - assign a value *different* from all other EC's if the type is infinite
- // Assign first value from type enumerator otherwise - for finite types, we rely on polite framework to ensure that EC's that have to be
- // different are different.
-
- // Only make assignments on a type if:
- // 1. fullModel is true
- // 2. there are no terms that share the same base type with un-normalized representatives
- // 3. there are no terms that share teh same base type that are unevaluated evaluable terms
- // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment
- changed = false;
- for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
- set<Node>& noRepSet = TypeSet::getSet(it);
- if (noRepSet.empty()) {
- continue;
- }
- TypeNode t = TypeSet::getType(it);
- TypeNode tb = t.getBaseType();
- if (!assignOne) {
- set<Node>* repSet = typeRepSet.getSet(tb);
- if (repSet != NULL && !repSet->empty()) {
- continue;
- }
- if (evaluableSet.find(tb) != evaluableSet.end()) {
- continue;
- }
- }
- Trace("model-builder") << " Assign phase, working on type: " << t << endl;
- bool assignable, evaluable CVC4_UNUSED;
- for (i = noRepSet.begin(); i != noRepSet.end(); ) {
- i2 = i;
- ++i;
- eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine);
- assignable = false;
- evaluable = false;
- for ( ; !eqc_i.isFinished(); ++eqc_i) {
- Node n = *eqc_i;
- if (isAssignable(n)) {
- assignable = true;
- }
- else {
- evaluable = true;
- }
- }
- if (assignable) {
- Assert(!evaluable || assignOne);
- Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
- Node n;
- if (t.getCardinality().isInfinite()) {
- n = typeConstSet.nextTypeEnum(t, true);
- }
- else {
- TypeEnumerator te(t);
- n = *te;
- }
- Assert(!n.isNull());
- constantReps[*i2] = n;
- Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl;
- changed = true;
- noRepSet.erase(i2);
- if (assignOne) {
- assignOne = false;
- break;
- }
- }
- }
- }
-
- // Corner case - I'm not sure this can even happen - but it's theoretically possible to have a cyclical dependency
- // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In this case, neither one will get assigned because we are waiting
- // to be able to evaluate. But we will never be able to evaluate because the variables that need to be assigned are in
- // these same EC's. In this case, repeat the whole fixed-point computation with the difference that the first EC
- // that has both assignable and evaluable expressions will get assigned.
- if (!changed) {
- Assert(!assignOne); // check for infinite loop!
- assignOne = true;
- }
- }
-
-#ifdef CVC4_ASSERTIONS
- if (fullModel) {
- // Assert that all representatives have been converted to constants
- for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
- set<Node>& repSet = TypeSet::getSet(it);
- if (!repSet.empty()) {
- Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl;
- Assert(false);
- }
- }
- }
-#endif /* CVC4_ASSERTIONS */
-
- Trace("model-builder") << "Copy representatives to model..." << std::endl;
- tm->d_reps.clear();
- std::map< Node, Node >::iterator itMap;
- for (itMap = constantReps.begin(); itMap != constantReps.end(); ++itMap) {
- tm->d_reps[itMap->first] = itMap->second;
- tm->d_rep_set.add(itMap->second);
- }
-
- if (!fullModel) {
- Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
- // Make sure every EC has a rep
- for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) {
- tm->d_reps[itMap->first] = itMap->second;
- tm->d_rep_set.add(itMap->second);
- }
- for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
- set<Node>& noRepSet = TypeSet::getSet(it);
- set<Node>::iterator i;
- for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
- tm->d_reps[*i] = *i;
- tm->d_rep_set.add(*i);
- }
- }
- }
-
- //modelBuilder-specific initialization
- processBuildModel( tm, fullModel );
-
-#ifdef CVC4_ASSERTIONS
- if (fullModel) {
- // Check that every term evaluates to its representative in the model
- for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) {
- // eqc is the equivalence class representative
- Node eqc = (*eqcs_i);
- Node rep;
- itMap = constantReps.find(eqc);
- if (itMap == constantReps.end() && eqc.getType().isBoolean()) {
- rep = tm->getValue(eqc);
- Assert(rep.isConst());
- }
- else {
- Assert(itMap != constantReps.end());
- rep = itMap->second;
- }
- eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
- for ( ; !eqc_i.isFinished(); ++eqc_i) {
- Node n = *eqc_i;
- static int repCheckInstance = 0;
- ++repCheckInstance;
-
- Debug("check-model::rep-checking")
- << "( " << repCheckInstance <<") "
- << "n: " << n << endl
- << "getValue(n): " << tm->getValue(n) << endl
- << "rep: " << rep << endl;
- Assert(tm->getValue(*eqc_i) == rep);
- }
- }
- }
-#endif /* CVC4_ASSERTIONS */
-}
-
-
-Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps, bool evalOnly)
-{
- std::map<Node, Node>::iterator itMap = constantReps.find(r);
- if (itMap != constantReps.end()) {
- return (*itMap).second;
- }
- NodeMap::iterator it = d_normalizedCache.find(r);
- if (it != d_normalizedCache.end()) {
- return (*it).second;
- }
- Node retNode = r;
- if (r.getNumChildren() > 0) {
- std::vector<Node> children;
- if (r.getMetaKind() == kind::metakind::PARAMETERIZED) {
- children.push_back(r.getOperator());
- }
- bool childrenConst = true;
- for (size_t i=0; i < r.getNumChildren(); ++i) {
- Node ri = r[i];
- bool recurse = true;
- if (!ri.isConst()) {
- if (m->d_equalityEngine->hasTerm(ri)) {
- itMap = constantReps.find(m->d_equalityEngine->getRepresentative(ri));
- if (itMap != constantReps.end()) {
- ri = (*itMap).second;
- recurse = false;
- }
- else if (!evalOnly) {
- recurse = false;
- }
- }
- if (recurse) {
- ri = normalize(m, ri, constantReps, evalOnly);
- }
- if (!ri.isConst()) {
- childrenConst = false;
- }
- }
- children.push_back(ri);
- }
- retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
- if (childrenConst) {
- retNode = Rewriter::rewrite(retNode);
- Assert(retNode.getKind() == kind::APPLY_UF || retNode.isConst());
- }
- }
- d_normalizedCache[r] = retNode;
- return retNode;
-}
-
-
-void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel)
-{
- if (fullModel) {
- Trace("model-builder") << "Assigning function values..." << endl;
- //construct function values
- for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
- Node n = it->first;
- if( m->d_uf_models.find( n )==m->d_uf_models.end() ){
- TypeNode type = n.getType();
- uf::UfModelTree ufmt( n );
- Node default_v, un, simp, v;
- for( size_t i=0; i<it->second.size(); i++ ){
- un = it->second[i];
- vector<TNode> children;
- children.push_back(n);
- for (size_t j = 0; j < un.getNumChildren(); ++j) {
- children.push_back(m->getRepresentative(un[j]));
- }
- simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
- v = m->getRepresentative(un);
- Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")" << endl;
- ufmt.setValue(m, simp, v);
- default_v = v;
- }
- if( default_v.isNull() ){
- //choose default value from model if none exists
- TypeEnumerator te(type.getRangeType());
- default_v = (*te);
- }
- ufmt.setDefaultValue( m, default_v );
- if(options::condenseFunctionValues()) {
- ufmt.simplify();
- }
- Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() );
- Trace("model-builder") << " Assigning (" << n << ") to (" << val << ")" << endl;
- m->d_uf_models[n] = val;
- //ufmt.debugPrint( std::cout, m );
- }
- }
- }
-}
+++ /dev/null
-/********************* */
-/*! \file model.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters, Clark Barrett
- ** Minor contributors (to current version): Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Model class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_MODEL_H
-#define __CVC4__THEORY_MODEL_H
-
-#include "util/util_model.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/rep_set.h"
-#include "theory/substitutions.h"
-#include "theory/type_enumerator.h"
-
-namespace CVC4 {
-
-namespace theory {
-
-
-/** Theory Model class
- * For Model m, should call m.initialize() before using
- */
-class TheoryModel : public Model
-{
- friend class TheoryEngineModelBuilder;
-protected:
- /** substitution map for this model */
- SubstitutionMap d_substitutions;
-public:
- TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
- virtual ~TheoryModel(){}
-
- /** special local context for our equalityEngine so we can clear it independently of search context */
- context::Context* d_eeContext;
- /** equality engine containing all known equalities/disequalities */
- eq::EqualityEngine* d_equalityEngine;
- /** map of representatives of equality engine to used representatives in representative set */
- std::map< Node, Node > d_reps;
- /** stores set of representatives for each type */
- RepSet d_rep_set;
- /** true/false nodes */
- Node d_true;
- Node d_false;
- context::CDO<bool> d_modelBuilt;
-
-protected:
- /** reset the model */
- virtual void reset();
- /**
- * Get model value function. This function is called by getValue
- */
- Node getModelValue(TNode n, bool hasBoundVars = false) const;
-public:
- /**
- * Get value function. This should be called only after a ModelBuilder has called buildModel(...)
- * on this model.
- */
- Node getValue( TNode n ) const;
-
- /** get existing domain value, with possible exclusions
- * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
- */
- Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );
- /** get new domain value
- * This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn]
- * If it cannot find such a node, it returns null.
- */
- Node getNewDomainValue( TypeNode tn );
- /** complete all values for type
- * Calling this function ensures that all terms of type tn exist in d_rep_set.d_type_reps[tn]
- */
- void completeDomainValues( TypeNode tn ){
- d_rep_set.complete( tn );
- }
-public:
- /** Adds a substitution from x to t. */
- void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
- /** add term function
- * addTerm( n ) will do any model-specific processing necessary for n,
- * such as constraining the interpretation of uninterpreted functions,
- * and adding n to the equality engine of this model
- */
- virtual void addTerm(TNode n);
- /** assert equality holds in the model */
- void assertEquality(TNode a, TNode b, bool polarity);
- /** assert predicate holds in the model */
- void assertPredicate(TNode a, bool polarity);
- /** assert all equalities/predicates in equality engine hold in the model */
- void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL);
- /** assert representative
- * This function tells the model that n should be the representative of its equivalence class.
- * It should be called during model generation, before final representatives are chosen. In the
- * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... )
- * functions where fullModel = true.
- */
- void assertRepresentative(TNode n);
-public:
- /** general queries */
- bool hasTerm(TNode a);
- Node getRepresentative(TNode a);
- bool areEqual(TNode a, TNode b);
- bool areDisequal(TNode a, TNode b);
-public:
- /** get value function for Exprs. */
- Expr getValue( Expr expr ) const;
- /** get cardinality for sort */
- Cardinality getCardinality( Type t ) const;
-public:
- /** print representative debug function */
- void printRepresentativeDebug( const char* c, Node r );
- /** print representative function */
- void printRepresentative( std::ostream& out, Node r );
-public:
- /** whether function models are enabled */
- bool d_enableFuncModels;
- //necessary information for function models
- std::map< Node, std::vector< Node > > d_uf_terms;
- std::map< Node, Node > d_uf_models;
-};
-
-/*
- * Class that encapsulates a map from types to sets of nodes
- */
-class TypeSet {
-public:
- typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
- typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
- typedef TypeSetMap::iterator iterator;
- typedef TypeSetMap::const_iterator const_iterator;
-private:
- TypeSetMap d_typeSet;
- TypeToTypeEnumMap d_teMap;
-
- public:
- ~TypeSet() {
- iterator it;
- for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) {
- if ((*it).second != NULL) {
- delete (*it).second;
- }
- }
- TypeToTypeEnumMap::iterator it2;
- for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2) {
- if ((*it2).second != NULL) {
- delete (*it2).second;
- }
- }
- }
-
- void add(TypeNode t, TNode n)
- {
- iterator it = d_typeSet.find(t);
- std::set<Node>* s;
- if (it == d_typeSet.end()) {
- s = new std::set<Node>;
- d_typeSet[t] = s;
- }
- else {
- s = (*it).second;
- }
- s->insert(n);
- }
-
- std::set<Node>* getSet(TypeNode t) const
- {
- const_iterator it = d_typeSet.find(t);
- if (it == d_typeSet.end()) {
- return NULL;
- }
- return (*it).second;
- }
-
- Node nextTypeEnum(TypeNode t, bool useBaseType = false)
- {
- TypeEnumerator* te;
- TypeToTypeEnumMap::iterator it = d_teMap.find(t);
- if (it == d_teMap.end()) {
- te = new TypeEnumerator(t);
- d_teMap[t] = te;
- }
- else {
- te = (*it).second;
- }
- if (te->isFinished()) {
- return Node();
- }
-
- if (useBaseType) {
- t = t.getBaseType();
- }
- iterator itSet = d_typeSet.find(t);
- std::set<Node>* s;
- if (itSet == d_typeSet.end()) {
- s = new std::set<Node>;
- d_typeSet[t] = s;
- }
- else {
- s = (*itSet).second;
- }
- Node n = **te;
- while (s->find(n) != s->end()) {
- ++(*te);
- if (te->isFinished()) {
- return Node();
- }
- n = **te;
- }
- s->insert(n);
- ++(*te);
- return n;
- }
-
- bool empty()
- {
- return d_typeSet.empty();
- }
-
- iterator begin()
- {
- return d_typeSet.begin();
- }
-
- iterator end()
- {
- return d_typeSet.end();
- }
-
- static TypeNode getType(iterator it)
- {
- return (*it).first;
- }
-
- static std::set<Node>& getSet(iterator it)
- {
- return *(*it).second;
- }
-
-};
-
-/** TheoryEngineModelBuilder class
- * This model builder will consult all theories in a theory engine for
- * collectModelInfo( ... ) when building a model.
- */
-class TheoryEngineModelBuilder : public ModelBuilder
-{
-protected:
- /** pointer to theory engine */
- TheoryEngine* d_te;
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
- NodeMap d_normalizedCache;
- typedef std::hash_set<Node, NodeHashFunction> NodeSet;
-
- /** process build model */
- virtual void processBuildModel(TheoryModel* m, bool fullModel);
- /** normalize representative */
- Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
- bool isAssignable(TNode n);
- void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
-
-public:
- TheoryEngineModelBuilder(TheoryEngine* te);
- virtual ~TheoryEngineModelBuilder(){}
- /** Build model function.
- * Should be called only on TheoryModels m
- */
- void buildModel(Model* m, bool fullModel);
-};
-
-}
-}
-
-#endif
#ifndef __CVC4__FIRST_ORDER_MODEL_H
#define __CVC4__FIRST_ORDER_MODEL_H
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"
namespace CVC4 {
#define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
#include "theory/quantifiers_engine.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"
namespace CVC4 {
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/model_builder.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/quantifiers/full_model_check.h"
#include "theory/quantifiers/relevant_domain.h"
** \todo document this file
**/
-#pragma once
-
#include "cvc4_private.h"
+#pragma once
+
#include "expr/node.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
#include "expr/kind.h"
#include "theory/rewriter.h"
#include "expr/command.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "smt/logic_exception.h"
#include "theory/strings/options.h"
#include "theory/strings/type_enumerator.h"
#include "theory/ite_utilities.h"
#include "theory/unconstrained_simplifier.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
+
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/theory_quantifiers.h"
#include "theory/quantifiers/options.h"
bool alreadyVisited(TNode current, TNode parent) {
// Check if already visited
- d_visited.find(current) != d_visited.end();
+ if (d_visited.find(current) != d_visited.end()) return true;
// Don't visit non-boolean
if (!current.getType().isBoolean()) return true;
// New node
--- /dev/null
+/********************* */
+/*! \file theory_model.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters, Clark Barrett
+ ** Minor contributors (to current version): Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of model class
+ **/
+
+#include "theory/theory_model.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/type_enumerator.h"
+#include "smt/options.h"
+#include "smt/smt_engine.h"
+#include "theory/uf/theory_uf_model.h"
+#include "theory/uf/options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+
+TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) :
+ d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
+{
+ d_true = NodeManager::currentNM()->mkConst( true );
+ d_false = NodeManager::currentNM()->mkConst( false );
+
+ d_eeContext = new context::Context();
+ d_equalityEngine = new eq::EqualityEngine(d_eeContext, name);
+
+ // The kinds we are treating as function application in congruence
+ d_equalityEngine->addFunctionKind(kind::APPLY_UF);
+ d_equalityEngine->addFunctionKind(kind::SELECT);
+ // d_equalityEngine->addFunctionKind(kind::STORE);
+ d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
+ d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
+ d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
+ d_eeContext->push();
+}
+
+void TheoryModel::reset(){
+ d_reps.clear();
+ d_rep_set.clear();
+ d_uf_terms.clear();
+ d_uf_models.clear();
+ d_eeContext->pop();
+ d_eeContext->push();
+}
+
+Node TheoryModel::getValue(TNode n) const {
+ //apply substitutions
+ Node nn = d_substitutions.apply(n);
+ //get value in model
+ nn = getModelValue(nn);
+ if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
+ //normalize
+ nn = Rewriter::rewrite(nn);
+ }
+ return nn;
+}
+
+Expr TheoryModel::getValue( Expr expr ) const{
+ Node n = Node::fromExpr( expr );
+ Node ret = getValue( n );
+ return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr();
+}
+
+/** get cardinality for sort */
+Cardinality TheoryModel::getCardinality( Type t ) const{
+ TypeNode tn = TypeNode::fromType( t );
+ //for now, we only handle cardinalities for uninterpreted sorts
+ if( tn.isSort() ){
+ if( d_rep_set.hasType( tn ) ){
+ return Cardinality( d_rep_set.getNumRepresentatives( tn ) );
+ }else{
+ return Cardinality( CardinalityUnknown() );
+ }
+ }else{
+ return Cardinality( CardinalityUnknown() );
+ }
+}
+
+Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
+{
+ if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL) {
+ // We should have terms, thanks to TheoryQuantifiers::collectModelInfo().
+ // However, if the Decision Engine stops us early, there might be a
+ // quantifier that isn't assigned. In conjunction with miniscoping, this
+ // might lead to a perfectly good model. Think of
+ // ASSERT FORALL(x) : p OR x=5
+ // The p is pulled out by miniscoping, and set to TRUE by the decision
+ // engine, then the quantifier's value in the model doesn't matter, so the
+ // Decision Engine stops. So even though the top-level quantifier was
+ // asserted, it can't be checked directly: first, it doesn't "exist" in
+ // non-miniscoped form, and second, no quantifiers have been asserted, so
+ // none is in the model. We used to fail an assertion here, but that's
+ // no good. Instead, return the quantifier itself. If we're in
+ // checkModel(), and the quantifier actually matters, we'll get an
+ // assert-fail since the quantifier isn't a constant.
+ if(!d_equalityEngine->hasTerm(Rewriter::rewrite(n))) {
+ return n;
+ } else {
+ n = Rewriter::rewrite(n);
+ }
+ } else {
+ if(n.getKind() == kind::LAMBDA) {
+ NodeManager* nm = NodeManager::currentNM();
+ Node body = getModelValue(n[1], true);
+ body = Rewriter::rewrite(body);
+ return nm->mkNode(kind::LAMBDA, n[0], body);
+ }
+ if(n.isConst() || (hasBoundVars && n.getKind() == kind::BOUND_VARIABLE)) {
+ return n;
+ }
+
+ TypeNode t = n.getType();
+ if (t.isFunction() || t.isPredicate()) {
+ if (d_enableFuncModels) {
+ std::map< Node, Node >::const_iterator it = d_uf_models.find(n);
+ if (it != d_uf_models.end()) {
+ // Existing function
+ return it->second;
+ }
+ // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
+ vector<TypeNode> argTypes = t.getArgTypes();
+ vector<Node> args;
+ NodeManager* nm = NodeManager::currentNM();
+ for (unsigned i = 0; i < argTypes.size(); ++i) {
+ args.push_back(nm->mkBoundVar(argTypes[i]));
+ }
+ Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
+ TypeEnumerator te(t.getRangeType());
+ return nm->mkNode(kind::LAMBDA, boundVarList, *te);
+ }
+ // TODO: if func models not enabled, throw an error?
+ Unreachable();
+ }
+
+ if (n.getNumChildren() > 0) {
+ std::vector<Node> children;
+ if (n.getKind() == APPLY_UF) {
+ Node op = getModelValue(n.getOperator(), hasBoundVars);
+ children.push_back(op);
+ }
+ else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ children.push_back(n.getOperator());
+ }
+ //evaluate the children
+ for (unsigned i = 0; i < n.getNumChildren(); ++i) {
+ Node val = getModelValue(n[i], hasBoundVars);
+ children.push_back(val);
+ }
+ Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));
+ if(val.getKind() == kind::CARDINALITY_CONSTRAINT) {
+ val = NodeManager::currentNM()->mkConst(getCardinality(val[0].getType().toType()).getFiniteCardinality() <= val[1].getConst<Rational>().getNumerator());
+ }
+ if(val.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){
+ //FIXME
+ val = NodeManager::currentNM()->mkConst(false);
+ }
+ return val;
+ }
+
+ if (!d_equalityEngine->hasTerm(n)) {
+ // Unknown term - return first enumerated value for this type
+ TypeEnumerator te(n.getType());
+ return *te;
+ }
+ }
+ Node val = d_equalityEngine->getRepresentative(n);
+ Assert(d_reps.find(val) != d_reps.end());
+ std::map< Node, Node >::const_iterator it = d_reps.find( val );
+ if( it!=d_reps.end() ){
+ return it->second;
+ }else{
+ return Node::null();
+ }
+}
+
+Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
+ if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){
+ //try to find a pre-existing arbitrary element
+ for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){
+ if( std::find( exclude.begin(), exclude.end(), d_rep_set.d_type_reps[tn][i] )==exclude.end() ){
+ return d_rep_set.d_type_reps[tn][i];
+ }
+ }
+ }
+ return Node::null();
+}
+
+//FIXME: need to ensure that theory enumerators exist for each sort
+Node TheoryModel::getNewDomainValue( TypeNode tn ){
+ if( tn.isSort() ){
+ return Node::null();
+ }else{
+ TypeEnumerator te(tn);
+ while( !te.isFinished() ){
+ Node r = *te;
+ if(Debug.isOn("getNewDomainValue")) {
+ Debug("getNewDomainValue") << "getNewDomainValue( " << tn << ")" << endl;
+ Debug("getNewDomainValue") << "+ TypeEnumerator gave: " << r << endl;
+ Debug("getNewDomainValue") << "+ d_type_reps are:";
+ for(vector<Node>::const_iterator i = d_rep_set.d_type_reps[tn].begin();
+ i != d_rep_set.d_type_reps[tn].end();
+ ++i) {
+ Debug("getNewDomainValue") << " " << *i;
+ }
+ Debug("getNewDomainValue") << endl;
+ }
+ if( std::find(d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r) ==d_rep_set.d_type_reps[tn].end() ) {
+ Debug("getNewDomainValue") << "+ it's new, so returning " << r << endl;
+ return r;
+ }
+ ++te;
+ }
+ return Node::null();
+ }
+}
+
+/** add substitution */
+void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
+ if( !d_substitutions.hasSubstitution( x ) ){
+ d_substitutions.addSubstitution( x, t, invalidateCache );
+ } else {
+#ifdef CVC4_ASSERTIONS
+ Node oldX = d_substitutions.getSubstitution(x);
+ // check that either the old substitution is the same, or it now maps to the new substitution
+ if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) {
+ stringstream ss;
+ ss << "Two incompatible substitutions added to TheoryModel:\n"
+ << "the term: " << x << "\n"
+ << "old mapping: " << d_substitutions.apply(oldX) << "\n"
+ << "new mapping: " << d_substitutions.apply(t);
+ InternalError(ss.str());
+ }
+#endif /* CVC4_ASSERTIONS */
+ }
+}
+
+/** add term */
+void TheoryModel::addTerm(TNode n ){
+ Assert(d_equalityEngine->hasTerm(n));
+ //must collect UF terms
+ if (n.getKind()==APPLY_UF) {
+ Node op = n.getOperator();
+ if( std::find( d_uf_terms[ op ].begin(), d_uf_terms[ op ].end(), n )==d_uf_terms[ op ].end() ){
+ d_uf_terms[ op ].push_back( n );
+ Trace("model-add-term-uf") << "Add term " << n << std::endl;
+ }
+ }
+}
+
+/** assert equality */
+void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){
+ if (a == b && polarity) {
+ return;
+ }
+ Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl;
+ d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() );
+ Assert(d_equalityEngine->consistent());
+}
+
+/** assert predicate */
+void TheoryModel::assertPredicate(TNode a, bool polarity ){
+ if ((a == d_true && polarity) ||
+ (a == d_false && (!polarity))) {
+ return;
+ }
+ if (a.getKind() == EQUAL) {
+ Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl;
+ d_equalityEngine->assertEquality( a, polarity, Node::null() );
+ } else {
+ Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl;
+ d_equalityEngine->assertPredicate( a, polarity, Node::null() );
+ Assert(d_equalityEngine->consistent());
+ }
+}
+
+/** assert equality engine */
+void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* termSet)
+{
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+ for (; !eqcs_i.isFinished(); ++eqcs_i) {
+ Node eqc = (*eqcs_i);
+ bool predicate = false;
+ bool predTrue = false;
+ bool predFalse = false;
+ if (eqc.getType().isBoolean()) {
+ predicate = true;
+ predTrue = ee->areEqual(eqc, d_true);
+ predFalse = ee->areEqual(eqc, d_false);
+ }
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
+ bool first = true;
+ Node rep;
+ for (; !eqc_i.isFinished(); ++eqc_i) {
+ if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) {
+ continue;
+ }
+ if (predicate) {
+ if (predTrue) {
+ assertPredicate(*eqc_i, true);
+ }
+ else if (predFalse) {
+ assertPredicate(*eqc_i, false);
+ }
+ else {
+ if (first) {
+ rep = (*eqc_i);
+ first = false;
+ }
+ else {
+ Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl;
+ d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null());
+ Assert(d_equalityEngine->consistent());
+ }
+ }
+ } else {
+ if (first) {
+ rep = (*eqc_i);
+ first = false;
+ }
+ else {
+ assertEquality(*eqc_i, rep, true);
+ }
+ }
+ }
+ }
+}
+
+void TheoryModel::assertRepresentative(TNode n )
+{
+ Trace("model-builder-reps") << "Assert rep : " << n << std::endl;
+ d_reps[ n ] = n;
+}
+
+bool TheoryModel::hasTerm(TNode a)
+{
+ return d_equalityEngine->hasTerm( a );
+}
+
+Node TheoryModel::getRepresentative(TNode a)
+{
+ if( d_equalityEngine->hasTerm( a ) ){
+ Node r = d_equalityEngine->getRepresentative( a );
+ if( d_reps.find( r )!=d_reps.end() ){
+ return d_reps[ r ];
+ }else{
+ return r;
+ }
+ }else{
+ return a;
+ }
+}
+
+bool TheoryModel::areEqual(TNode a, TNode b)
+{
+ if( a==b ){
+ return true;
+ }else if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){
+ return d_equalityEngine->areEqual( a, b );
+ }else{
+ return false;
+ }
+}
+
+bool TheoryModel::areDisequal(TNode a, TNode b)
+{
+ if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){
+ return d_equalityEngine->areDisequal( a, b, false );
+ }else{
+ return false;
+ }
+}
+
+//for debugging
+void TheoryModel::printRepresentativeDebug( const char* c, Node r ){
+ if( r.isNull() ){
+ Trace( c ) << "null";
+ }else if( r.getType().isBoolean() ){
+ if( areEqual( r, d_true ) ){
+ Trace( c ) << "true";
+ }else{
+ Trace( c ) << "false";
+ }
+ }else{
+ Trace( c ) << getRepresentative( r );
+ }
+}
+
+void TheoryModel::printRepresentative( std::ostream& out, Node r ){
+ Assert( !r.isNull() );
+ if( r.isNull() ){
+ out << "null";
+ }else if( r.getType().isBoolean() ){
+ if( areEqual( r, d_true ) ){
+ out << "true";
+ }else{
+ out << "false";
+ }
+ }else{
+ out << getRepresentative( r );
+ }
+}
+
+
+TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){
+
+}
+
+
+bool TheoryEngineModelBuilder::isAssignable(TNode n)
+{
+ return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR);
+}
+
+
+void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache)
+{
+ if (n.getKind()==FORALL || n.getKind()==EXISTS) {
+ return;
+ }
+ if (cache.find(n) != cache.end()) {
+ return;
+ }
+ if (isAssignable(n)) {
+ tm->d_equalityEngine->addTerm(n);
+ }
+ for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
+ checkTerms(*child_it, tm, cache);
+ }
+ cache.insert(n);
+}
+
+
+void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
+{
+ Trace("model-builder") << "TheoryEngineModelBuilder: buildModel, fullModel = " << fullModel << std::endl;
+ TheoryModel* tm = (TheoryModel*)m;
+
+ // buildModel with fullModel = true should only be called once in any context
+ Assert(!tm->d_modelBuilt);
+ tm->d_modelBuilt = fullModel;
+
+ // Reset model
+ tm->reset();
+
+ // Collect model info from the theories
+ Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
+ d_te->collectModelInfo(tm, fullModel);
+
+ // Loop through all terms and make sure that assignable sub-terms are in the equality engine
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine );
+ {
+ NodeSet cache;
+ for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
+ eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i),tm->d_equalityEngine);
+ for ( ; !eqc_i.isFinished(); ++eqc_i) {
+ checkTerms(*eqc_i, tm, cache);
+ }
+ }
+ }
+
+ Trace("model-builder") << "Collect representatives..." << std::endl;
+
+ // Process all terms in the equality engine, store representatives for each EC
+ std::map< Node, Node > assertedReps, constantReps;
+ TypeSet typeConstSet, typeRepSet, typeNoRepSet;
+ std::set< TypeNode > allTypes;
+ eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
+ for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
+
+ // eqc is the equivalence class representative
+ Node eqc = (*eqcs_i);
+ Trace("model-builder") << "Processing EC: " << eqc << endl;
+ Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
+ TypeNode eqct = eqc.getType();
+ Assert(assertedReps.find(eqc) == assertedReps.end());
+ Assert(constantReps.find(eqc) == constantReps.end());
+
+ // Loop through terms in this EC
+ Node rep, const_rep;
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
+ for ( ; !eqc_i.isFinished(); ++eqc_i) {
+ Node n = *eqc_i;
+ Trace("model-builder") << " Processing Term: " << n << endl;
+ // Record as rep if this node was specified as a representative
+ if (tm->d_reps.find(n) != tm->d_reps.end()){
+ Assert(rep.isNull());
+ rep = tm->d_reps[n];
+ Assert(!rep.isNull() );
+ Trace("model-builder") << " Rep( " << eqc << " ) = " << rep << std::endl;
+ }
+ // Record as const_rep if this node is constant
+ if (n.isConst()) {
+ Assert(const_rep.isNull());
+ const_rep = n;
+ Trace("model-builder") << " ConstRep( " << eqc << " ) = " << const_rep << std::endl;
+ }
+ //model-specific processing of the term
+ tm->addTerm(n);
+ }
+
+ // Assign representative for this EC
+ if (!const_rep.isNull()) {
+ // Theories should not specify a rep if there is already a constant in the EC
+ Assert(rep.isNull() || rep == const_rep);
+ constantReps[eqc] = const_rep;
+ typeConstSet.add(eqct.getBaseType(), const_rep);
+ }
+ else if (!rep.isNull()) {
+ assertedReps[eqc] = rep;
+ typeRepSet.add(eqct.getBaseType(), eqc);
+ allTypes.insert(eqct);
+ }
+ else {
+ typeNoRepSet.add(eqct, eqc);
+ allTypes.insert(eqct);
+ }
+ }
+
+ // Need to ensure that each EC has a constant representative.
+
+ Trace("model-builder") << "Processing EC's..." << std::endl;
+
+ TypeSet::iterator it;
+ set<TypeNode>::iterator type_it;
+ set<Node>::iterator i, i2;
+ bool changed, unassignedAssignable, assignOne = false;
+ set<TypeNode> evaluableSet;
+
+ // Double-fixed-point loop
+ // Outer loop handles a special corner case (see code at end of loop for details)
+ for (;;) {
+
+ // Inner fixed-point loop: we are trying to learn constant values for every EC. Each time through this loop, we process all of the
+ // types by type and may learn some new EC values. EC's in one type may depend on EC's in another type, so we need a fixed-point loop
+ // to ensure that we learn as many EC values as possible
+ do {
+ changed = false;
+ unassignedAssignable = false;
+ evaluableSet.clear();
+
+ // Iterate over all types we've seen
+ for (type_it = allTypes.begin(); type_it != allTypes.end(); ++type_it) {
+ TypeNode t = *type_it;
+ TypeNode tb = t.getBaseType();
+ set<Node>* noRepSet = typeNoRepSet.getSet(t);
+
+ // 1. Try to evaluate the EC's in this type
+ if (noRepSet != NULL && !noRepSet->empty()) {
+ Trace("model-builder") << " Eval phase, working on type: " << t << endl;
+ bool assignable, evaluable, evaluated;
+ d_normalizedCache.clear();
+ for (i = noRepSet->begin(); i != noRepSet->end(); ) {
+ i2 = i;
+ ++i;
+ assignable = false;
+ evaluable = false;
+ evaluated = false;
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine);
+ for ( ; !eqc_i.isFinished(); ++eqc_i) {
+ Node n = *eqc_i;
+ if (isAssignable(n)) {
+ assignable = true;
+ }
+ else {
+ evaluable = true;
+ Node normalized = normalize(tm, n, constantReps, true);
+ if (normalized.isConst()) {
+ typeConstSet.add(tb, normalized);
+ constantReps[*i2] = normalized;
+ Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
+ changed = true;
+ evaluated = true;
+ noRepSet->erase(i2);
+ break;
+ }
+ }
+ }
+ if (!evaluated) {
+ if (evaluable) {
+ evaluableSet.insert(tb);
+ }
+ if (assignable) {
+ unassignedAssignable = true;
+ }
+ }
+ }
+ }
+
+ // 2. Normalize any non-const representative terms for this type
+ set<Node>* repSet = typeRepSet.getSet(t);
+ if (repSet != NULL && !repSet->empty()) {
+ Trace("model-builder") << " Normalization phase, working on type: " << t << endl;
+ d_normalizedCache.clear();
+ for (i = repSet->begin(); i != repSet->end(); ) {
+ Assert(assertedReps.find(*i) != assertedReps.end());
+ Node rep = assertedReps[*i];
+ Node normalized = normalize(tm, rep, constantReps, false);
+ Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
+ if (normalized.isConst()) {
+ changed = true;
+ typeConstSet.add(t.getBaseType(), normalized);
+ constantReps[*i] = normalized;
+ assertedReps.erase(*i);
+ i2 = i;
+ ++i;
+ repSet->erase(i2);
+ }
+ else {
+ if (normalized != rep) {
+ assertedReps[*i] = normalized;
+ changed = true;
+ }
+ ++i;
+ }
+ }
+ }
+ }
+ } while (changed);
+
+ if (!fullModel || !unassignedAssignable) {
+ break;
+ }
+
+ // 3. Assign unassigned assignable EC's using type enumeration - assign a value *different* from all other EC's if the type is infinite
+ // Assign first value from type enumerator otherwise - for finite types, we rely on polite framework to ensure that EC's that have to be
+ // different are different.
+
+ // Only make assignments on a type if:
+ // 1. fullModel is true
+ // 2. there are no terms that share the same base type with un-normalized representatives
+ // 3. there are no terms that share teh same base type that are unevaluated evaluable terms
+ // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment
+ changed = false;
+ for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
+ set<Node>& noRepSet = TypeSet::getSet(it);
+ if (noRepSet.empty()) {
+ continue;
+ }
+ TypeNode t = TypeSet::getType(it);
+ TypeNode tb = t.getBaseType();
+ if (!assignOne) {
+ set<Node>* repSet = typeRepSet.getSet(tb);
+ if (repSet != NULL && !repSet->empty()) {
+ continue;
+ }
+ if (evaluableSet.find(tb) != evaluableSet.end()) {
+ continue;
+ }
+ }
+ Trace("model-builder") << " Assign phase, working on type: " << t << endl;
+ bool assignable, evaluable CVC4_UNUSED;
+ for (i = noRepSet.begin(); i != noRepSet.end(); ) {
+ i2 = i;
+ ++i;
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine);
+ assignable = false;
+ evaluable = false;
+ for ( ; !eqc_i.isFinished(); ++eqc_i) {
+ Node n = *eqc_i;
+ if (isAssignable(n)) {
+ assignable = true;
+ }
+ else {
+ evaluable = true;
+ }
+ }
+ if (assignable) {
+ Assert(!evaluable || assignOne);
+ Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
+ Node n;
+ if (t.getCardinality().isInfinite()) {
+ n = typeConstSet.nextTypeEnum(t, true);
+ }
+ else {
+ TypeEnumerator te(t);
+ n = *te;
+ }
+ Assert(!n.isNull());
+ constantReps[*i2] = n;
+ Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl;
+ changed = true;
+ noRepSet.erase(i2);
+ if (assignOne) {
+ assignOne = false;
+ break;
+ }
+ }
+ }
+ }
+
+ // Corner case - I'm not sure this can even happen - but it's theoretically possible to have a cyclical dependency
+ // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In this case, neither one will get assigned because we are waiting
+ // to be able to evaluate. But we will never be able to evaluate because the variables that need to be assigned are in
+ // these same EC's. In this case, repeat the whole fixed-point computation with the difference that the first EC
+ // that has both assignable and evaluable expressions will get assigned.
+ if (!changed) {
+ Assert(!assignOne); // check for infinite loop!
+ assignOne = true;
+ }
+ }
+
+#ifdef CVC4_ASSERTIONS
+ if (fullModel) {
+ // Assert that all representatives have been converted to constants
+ for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
+ set<Node>& repSet = TypeSet::getSet(it);
+ if (!repSet.empty()) {
+ Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl;
+ Assert(false);
+ }
+ }
+ }
+#endif /* CVC4_ASSERTIONS */
+
+ Trace("model-builder") << "Copy representatives to model..." << std::endl;
+ tm->d_reps.clear();
+ std::map< Node, Node >::iterator itMap;
+ for (itMap = constantReps.begin(); itMap != constantReps.end(); ++itMap) {
+ tm->d_reps[itMap->first] = itMap->second;
+ tm->d_rep_set.add(itMap->second);
+ }
+
+ if (!fullModel) {
+ Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
+ // Make sure every EC has a rep
+ for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) {
+ tm->d_reps[itMap->first] = itMap->second;
+ tm->d_rep_set.add(itMap->second);
+ }
+ for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
+ set<Node>& noRepSet = TypeSet::getSet(it);
+ set<Node>::iterator i;
+ for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
+ tm->d_reps[*i] = *i;
+ tm->d_rep_set.add(*i);
+ }
+ }
+ }
+
+ //modelBuilder-specific initialization
+ processBuildModel( tm, fullModel );
+
+#ifdef CVC4_ASSERTIONS
+ if (fullModel) {
+ // Check that every term evaluates to its representative in the model
+ for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) {
+ // eqc is the equivalence class representative
+ Node eqc = (*eqcs_i);
+ Node rep;
+ itMap = constantReps.find(eqc);
+ if (itMap == constantReps.end() && eqc.getType().isBoolean()) {
+ rep = tm->getValue(eqc);
+ Assert(rep.isConst());
+ }
+ else {
+ Assert(itMap != constantReps.end());
+ rep = itMap->second;
+ }
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
+ for ( ; !eqc_i.isFinished(); ++eqc_i) {
+ Node n = *eqc_i;
+ static int repCheckInstance = 0;
+ ++repCheckInstance;
+
+ Debug("check-model::rep-checking")
+ << "( " << repCheckInstance <<") "
+ << "n: " << n << endl
+ << "getValue(n): " << tm->getValue(n) << endl
+ << "rep: " << rep << endl;
+ Assert(tm->getValue(*eqc_i) == rep);
+ }
+ }
+ }
+#endif /* CVC4_ASSERTIONS */
+}
+
+
+Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps, bool evalOnly)
+{
+ std::map<Node, Node>::iterator itMap = constantReps.find(r);
+ if (itMap != constantReps.end()) {
+ return (*itMap).second;
+ }
+ NodeMap::iterator it = d_normalizedCache.find(r);
+ if (it != d_normalizedCache.end()) {
+ return (*it).second;
+ }
+ Node retNode = r;
+ if (r.getNumChildren() > 0) {
+ std::vector<Node> children;
+ if (r.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ children.push_back(r.getOperator());
+ }
+ bool childrenConst = true;
+ for (size_t i=0; i < r.getNumChildren(); ++i) {
+ Node ri = r[i];
+ bool recurse = true;
+ if (!ri.isConst()) {
+ if (m->d_equalityEngine->hasTerm(ri)) {
+ itMap = constantReps.find(m->d_equalityEngine->getRepresentative(ri));
+ if (itMap != constantReps.end()) {
+ ri = (*itMap).second;
+ recurse = false;
+ }
+ else if (!evalOnly) {
+ recurse = false;
+ }
+ }
+ if (recurse) {
+ ri = normalize(m, ri, constantReps, evalOnly);
+ }
+ if (!ri.isConst()) {
+ childrenConst = false;
+ }
+ }
+ children.push_back(ri);
+ }
+ retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
+ if (childrenConst) {
+ retNode = Rewriter::rewrite(retNode);
+ Assert(retNode.getKind() == kind::APPLY_UF || retNode.isConst());
+ }
+ }
+ d_normalizedCache[r] = retNode;
+ return retNode;
+}
+
+
+void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel)
+{
+ if (fullModel) {
+ Trace("model-builder") << "Assigning function values..." << endl;
+ //construct function values
+ for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
+ Node n = it->first;
+ if( m->d_uf_models.find( n )==m->d_uf_models.end() ){
+ TypeNode type = n.getType();
+ uf::UfModelTree ufmt( n );
+ Node default_v, un, simp, v;
+ for( size_t i=0; i<it->second.size(); i++ ){
+ un = it->second[i];
+ vector<TNode> children;
+ children.push_back(n);
+ for (size_t j = 0; j < un.getNumChildren(); ++j) {
+ children.push_back(m->getRepresentative(un[j]));
+ }
+ simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
+ v = m->getRepresentative(un);
+ Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")" << endl;
+ ufmt.setValue(m, simp, v);
+ default_v = v;
+ }
+ if( default_v.isNull() ){
+ //choose default value from model if none exists
+ TypeEnumerator te(type.getRangeType());
+ default_v = (*te);
+ }
+ ufmt.setDefaultValue( m, default_v );
+ if(options::condenseFunctionValues()) {
+ ufmt.simplify();
+ }
+ Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() );
+ Trace("model-builder") << " Assigning (" << n << ") to (" << val << ")" << endl;
+ m->d_uf_models[n] = val;
+ //ufmt.debugPrint( std::cout, m );
+ }
+ }
+ }
+}
--- /dev/null
+/********************* */
+/*! \file theory_model.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: Morgan Deters, Clark Barrett
+ ** Minor contributors (to current version): Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Model class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__THEORY_MODEL_H
+#define __CVC4__THEORY__THEORY_MODEL_H
+
+#include "util/model.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/rep_set.h"
+#include "theory/substitutions.h"
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * Theory Model class.
+ * For Model m, should call m.initialize() before using.
+ */
+class TheoryModel : public Model
+{
+ friend class TheoryEngineModelBuilder;
+protected:
+ /** substitution map for this model */
+ SubstitutionMap d_substitutions;
+public:
+ TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
+ virtual ~TheoryModel(){}
+
+ /** special local context for our equalityEngine so we can clear it independently of search context */
+ context::Context* d_eeContext;
+ /** equality engine containing all known equalities/disequalities */
+ eq::EqualityEngine* d_equalityEngine;
+ /** map of representatives of equality engine to used representatives in representative set */
+ std::map< Node, Node > d_reps;
+ /** stores set of representatives for each type */
+ RepSet d_rep_set;
+ /** true/false nodes */
+ Node d_true;
+ Node d_false;
+ context::CDO<bool> d_modelBuilt;
+
+protected:
+ /** reset the model */
+ virtual void reset();
+ /**
+ * Get model value function. This function is called by getValue
+ */
+ Node getModelValue(TNode n, bool hasBoundVars = false) const;
+public:
+ /**
+ * Get value function. This should be called only after a ModelBuilder has called buildModel(...)
+ * on this model.
+ */
+ Node getValue( TNode n ) const;
+
+ /** get existing domain value, with possible exclusions
+ * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
+ */
+ Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );
+ /** get new domain value
+ * This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn]
+ * If it cannot find such a node, it returns null.
+ */
+ Node getNewDomainValue( TypeNode tn );
+ /** complete all values for type
+ * Calling this function ensures that all terms of type tn exist in d_rep_set.d_type_reps[tn]
+ */
+ void completeDomainValues( TypeNode tn ){
+ d_rep_set.complete( tn );
+ }
+public:
+ /** Adds a substitution from x to t. */
+ void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
+ /** add term function
+ * addTerm( n ) will do any model-specific processing necessary for n,
+ * such as constraining the interpretation of uninterpreted functions,
+ * and adding n to the equality engine of this model
+ */
+ virtual void addTerm(TNode n);
+ /** assert equality holds in the model */
+ void assertEquality(TNode a, TNode b, bool polarity);
+ /** assert predicate holds in the model */
+ void assertPredicate(TNode a, bool polarity);
+ /** assert all equalities/predicates in equality engine hold in the model */
+ void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL);
+ /** assert representative
+ * This function tells the model that n should be the representative of its equivalence class.
+ * It should be called during model generation, before final representatives are chosen. In the
+ * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... )
+ * functions where fullModel = true.
+ */
+ void assertRepresentative(TNode n);
+public:
+ /** general queries */
+ bool hasTerm(TNode a);
+ Node getRepresentative(TNode a);
+ bool areEqual(TNode a, TNode b);
+ bool areDisequal(TNode a, TNode b);
+public:
+ /** get value function for Exprs. */
+ Expr getValue( Expr expr ) const;
+ /** get cardinality for sort */
+ Cardinality getCardinality( Type t ) const;
+public:
+ /** print representative debug function */
+ void printRepresentativeDebug( const char* c, Node r );
+ /** print representative function */
+ void printRepresentative( std::ostream& out, Node r );
+public:
+ /** whether function models are enabled */
+ bool d_enableFuncModels;
+ //necessary information for function models
+ std::map< Node, std::vector< Node > > d_uf_terms;
+ std::map< Node, Node > d_uf_models;
+};/* class TheoryModel */
+
+/*
+ * Class that encapsulates a map from types to sets of nodes
+ */
+class TypeSet {
+public:
+ typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
+ typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
+ typedef TypeSetMap::iterator iterator;
+ typedef TypeSetMap::const_iterator const_iterator;
+private:
+ TypeSetMap d_typeSet;
+ TypeToTypeEnumMap d_teMap;
+
+ public:
+ ~TypeSet() {
+ iterator it;
+ for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) {
+ if ((*it).second != NULL) {
+ delete (*it).second;
+ }
+ }
+ TypeToTypeEnumMap::iterator it2;
+ for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2) {
+ if ((*it2).second != NULL) {
+ delete (*it2).second;
+ }
+ }
+ }
+
+ void add(TypeNode t, TNode n)
+ {
+ iterator it = d_typeSet.find(t);
+ std::set<Node>* s;
+ if (it == d_typeSet.end()) {
+ s = new std::set<Node>;
+ d_typeSet[t] = s;
+ }
+ else {
+ s = (*it).second;
+ }
+ s->insert(n);
+ }
+
+ std::set<Node>* getSet(TypeNode t) const
+ {
+ const_iterator it = d_typeSet.find(t);
+ if (it == d_typeSet.end()) {
+ return NULL;
+ }
+ return (*it).second;
+ }
+
+ Node nextTypeEnum(TypeNode t, bool useBaseType = false)
+ {
+ TypeEnumerator* te;
+ TypeToTypeEnumMap::iterator it = d_teMap.find(t);
+ if (it == d_teMap.end()) {
+ te = new TypeEnumerator(t);
+ d_teMap[t] = te;
+ }
+ else {
+ te = (*it).second;
+ }
+ if (te->isFinished()) {
+ return Node();
+ }
+
+ if (useBaseType) {
+ t = t.getBaseType();
+ }
+ iterator itSet = d_typeSet.find(t);
+ std::set<Node>* s;
+ if (itSet == d_typeSet.end()) {
+ s = new std::set<Node>;
+ d_typeSet[t] = s;
+ }
+ else {
+ s = (*itSet).second;
+ }
+ Node n = **te;
+ while (s->find(n) != s->end()) {
+ ++(*te);
+ if (te->isFinished()) {
+ return Node();
+ }
+ n = **te;
+ }
+ s->insert(n);
+ ++(*te);
+ return n;
+ }
+
+ bool empty()
+ {
+ return d_typeSet.empty();
+ }
+
+ iterator begin()
+ {
+ return d_typeSet.begin();
+ }
+
+ iterator end()
+ {
+ return d_typeSet.end();
+ }
+
+ static TypeNode getType(iterator it)
+ {
+ return (*it).first;
+ }
+
+ static std::set<Node>& getSet(iterator it)
+ {
+ return *(*it).second;
+ }
+
+};/* class TypeSet */
+
+/** TheoryEngineModelBuilder class
+ * This model builder will consult all theories in a theory engine for
+ * collectModelInfo( ... ) when building a model.
+ */
+class TheoryEngineModelBuilder : public ModelBuilder
+{
+protected:
+ /** pointer to theory engine */
+ TheoryEngine* d_te;
+ typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ NodeMap d_normalizedCache;
+ typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+
+ /** process build model */
+ virtual void processBuildModel(TheoryModel* m, bool fullModel);
+ /** normalize representative */
+ Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
+ bool isAssignable(TNode n);
+ void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
+
+public:
+ TheoryEngineModelBuilder(TheoryEngine* te);
+ virtual ~TheoryEngineModelBuilder(){}
+ /** Build model function.
+ * Should be called only on TheoryModels m
+ */
+ void buildModel(Model* m, bool fullModel);
+};/* class TheoryEngineModelBuilder */
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__THEORY_MODEL_H */
** kinds files to produce the final header.
**/
+#include "cvc4_private.h"
+
#pragma once
-#include "cvc4_private.h"
#include "theory/theory.h"
#include "theory/options.h"
#include "theory/uf/options.h"
#include "theory/quantifiers/options.h"
#include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/type_enumerator.h"
using namespace std;
#ifndef __CVC4__THEORY_UF_MODEL_H
#define __CVC4__THEORY_UF_MODEL_H
-#include "theory/model.h"
+#include "theory/theory_model.h"
namespace CVC4 {
namespace theory {
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/term_database.h"
#include "theory/uf/options.h"
-#include "theory/model.h"
+#include "theory/theory_model.h"
#include "theory/quantifiers/symmetry_breaking.h"
-
//#define ONE_SPLIT_REGION
//#define DISABLE_QUICK_CLIQUE_CHECKS
//#define COMBINE_REGIONS_SMALL_INTO_LARGE
abstract_value.cpp \
array_store_all.h \
array_store_all.cpp \
- util_model.h \
- util_model.cpp \
+ model.h \
+ model.cpp \
sort_inference.h \
sort_inference.cpp \
regexp.h
--- /dev/null
+/********************* */
+/*! \file model.cpp
+ ** \verbatim
+ ** Original author: Clark Barrett
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief implementation of Model class
+ **/
+
+#include "util/model.h"
+#include "expr/command.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/command_list.h"
+#include "printer/printer.h"
+
+#include <vector>
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const Model& m) {
+ smt::SmtScope smts(&m.d_smt);
+ Expr::dag::Scope scope(out, false);
+ Printer::getPrinter(options::outputLanguage())->toStream(out, m);
+ return out;
+}
+
+Model::Model() :
+ d_smt(*smt::currentSmtEngine()) {
+}
+
+size_t Model::getNumCommands() const {
+ return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size();
+}
+
+const Command* Model::getCommand(size_t i) const {
+ Assert(i < getNumCommands());
+ // index the global commands first, then the locals
+ if(i < d_smt.d_modelGlobalCommands.size()) {
+ return d_smt.d_modelGlobalCommands[i];
+ } else {
+ return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()];
+ }
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file model.h
+ ** \verbatim
+ ** Original author: Clark Barrett
+ ** Major contributors: Andrew Reynolds, Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Model class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__MODEL_H
+#define __CVC4__MODEL_H
+
+#include <iostream>
+#include <vector>
+
+#include "expr/expr.h"
+#include "util/cardinality.h"
+
+namespace CVC4 {
+
+class Command;
+class SmtEngine;
+class Model;
+
+std::ostream& operator<<(std::ostream&, const Model&);
+
+class Model {
+ friend std::ostream& operator<<(std::ostream&, const Model&);
+ friend class SmtEngine;
+
+ /** the input name (file name, etc.) this model is associated to */
+ std::string d_inputName;
+
+protected:
+ /** The SmtEngine we're associated with */
+ SmtEngine& d_smt;
+
+ /** construct the base class; users cannot do this, only CVC4 internals */
+ Model();
+
+public:
+ /** virtual destructor */
+ virtual ~Model() { }
+ /** get number of commands to report */
+ size_t getNumCommands() const;
+ /** get command */
+ const Command* getCommand(size_t i) const;
+ /** get the smt engine that this model is hooked up to */
+ SmtEngine* getSmtEngine() { return &d_smt; }
+ /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
+ const SmtEngine* getSmtEngine() const { return &d_smt; }
+ /** get the input name (file name, etc.) this model is associated to */
+ std::string getInputName() const { return d_inputName; }
+
+public:
+ /** get value for expression */
+ virtual Expr getValue(Expr expr) const = 0;
+ /** get cardinality for sort */
+ virtual Cardinality getCardinality(Type t) const = 0;
+};/* class Model */
+
+class ModelBuilder {
+public:
+ ModelBuilder() { }
+ virtual ~ModelBuilder() { }
+ virtual void buildModel(Model* m, bool fullModel) = 0;
+};/* class ModelBuilder */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__MODEL_H */
+++ /dev/null
-/********************* */
-/*! \file util_model.cpp
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief implementation of Model class
- **/
-
-#include "util/util_model.h"
-#include "expr/command.h"
-#include "smt/smt_engine_scope.h"
-#include "smt/command_list.h"
-#include "printer/printer.h"
-
-#include <vector>
-
-using namespace std;
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, const Model& m) {
- smt::SmtScope smts(&m.d_smt);
- Expr::dag::Scope scope(out, false);
- Printer::getPrinter(options::outputLanguage())->toStream(out, m);
- return out;
-}
-
-Model::Model() :
- d_smt(*smt::currentSmtEngine()) {
-}
-
-size_t Model::getNumCommands() const {
- return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size();
-}
-
-const Command* Model::getCommand(size_t i) const {
- Assert(i < getNumCommands());
- // index the global commands first, then the locals
- if(i < d_smt.d_modelGlobalCommands.size()) {
- return d_smt.d_modelGlobalCommands[i];
- } else {
- return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()];
- }
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file util_model.h
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: Andrew Reynolds, Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Model class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__UTIL_MODEL_H
-#define __CVC4__UTIL_MODEL_H
-
-#include <iostream>
-#include <vector>
-
-#include "expr/expr.h"
-#include "util/cardinality.h"
-
-namespace CVC4 {
-
-class Command;
-class SmtEngine;
-class Model;
-
-std::ostream& operator<<(std::ostream&, const Model&);
-
-class Model {
- friend std::ostream& operator<<(std::ostream&, const Model&);
- friend class SmtEngine;
-
- /** the input name (file name, etc.) this model is associated to */
- std::string d_inputName;
-
-protected:
- /** The SmtEngine we're associated with */
- SmtEngine& d_smt;
-
- /** construct the base class; users cannot do this, only CVC4 internals */
- Model();
-
-public:
- /** virtual destructor */
- virtual ~Model() { }
- /** get number of commands to report */
- size_t getNumCommands() const;
- /** get command */
- const Command* getCommand(size_t i) const;
- /** get the smt engine that this model is hooked up to */
- SmtEngine* getSmtEngine() { return &d_smt; }
- /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
- const SmtEngine* getSmtEngine() const { return &d_smt; }
- /** get the input name (file name, etc.) this model is associated to */
- std::string getInputName() const { return d_inputName; }
-
-public:
- /** get value for expression */
- virtual Expr getValue(Expr expr) const = 0;
- /** get cardinality for sort */
- virtual Cardinality getCardinality(Type t) const = 0;
-};/* class Model */
-
-class ModelBuilder {
-public:
- ModelBuilder() { }
- virtual ~ModelBuilder() { }
- virtual void buildModel(Model* m, bool fullModel) = 0;
-};/* class ModelBuilder */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__UTIL_MODEL_H */
projects / cvc5.git / commitdiff