From: Morgan Deters Date: Wed, 3 Jul 2013 21:13:31 +0000 (-0400) Subject: General pre-release cleanup commit X-Git-Tag: cvc5-1.0.0~7233 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a97891f9cc892fdc261cd4e3d3229ec68f05b45e;p=cvc5.git General pre-release cleanup commit * Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing --- diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT index 31ff2d47a..17affade4 100644 --- a/contrib/theoryskel/README.WHATS-NEXT +++ b/contrib/theoryskel/README.WHATS-NEXT @@ -6,7 +6,9 @@ Your next steps will likely be: * 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 diff --git a/src/Makefile.am b/src/Makefile.am index d6a0ffe0a..3637cb089 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -148,8 +148,8 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 8ae448657..3d5cec19b 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -29,7 +29,7 @@ #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" diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 4e476f4d9..cf72d4e4e 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -40,13 +40,10 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) 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; @@ -69,7 +66,7 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) switch(n.getKind()) { ${construles} -#line 73 "${template}" +#line 70 "${template}" default:; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 7667acdd0..786238492 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -22,7 +22,7 @@ #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" diff --git a/src/printer/printer.h b/src/printer/printer.h index 6fe1ec279..f73441966 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -21,7 +21,7 @@ #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" diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index d086caf38..869e02326 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -30,7 +30,7 @@ #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; diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 1157c464e..108c88829 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -18,7 +18,7 @@ #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" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2cc606fa9..2e1d5de3c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -70,7 +70,7 @@ #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" @@ -1815,7 +1815,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { 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; @@ -1904,7 +1904,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { Assert(d_topLevelSubstitutions.apply(t) == t); Assert(newSubstitutions.apply(t) == t); constantPropagations.addSubstitution(t, c); - // vector > equations;a + // vector > 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); @@ -1951,7 +1951,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { // } Assert(constantPropagations.apply((*pos).second) == (*pos).second); } -#endif +#endif /* CVC4_ASSERTIONS */ } // Resize the learnt d_nonClausalLearnedLiterals.resize(j); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 9d13dccb7..aa2b2a557 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -63,7 +63,7 @@ #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" diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 22fc8d4a7..86de3c1a9 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -71,7 +71,7 @@ #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" diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 45e18fe0d..0d3a578a6 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -100,7 +100,6 @@ public: 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); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 76e48aa1d..3aee02316 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -21,7 +21,7 @@ #include #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" diff --git a/src/theory/atom_requests.cpp b/src/theory/atom_requests.cpp index 3d111f9f8..6070004d2 100644 --- a/src/theory/atom_requests.cpp +++ b/src/theory/atom_requests.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \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; diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h index 99878125a..b54ece638 100644 --- a/src/theory/atom_requests.h +++ b/src/theory/atom_requests.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \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" diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 895f4a279..a809ad0e8 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -38,7 +38,7 @@ Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubsti 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(false)); diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 1caa4b429..00f183eb5 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -147,7 +147,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if ((*i).getKind() == kind::OR) done = false; } if (!done) { - return flattenNode(n, /*trivialNode = */ tt, /* skipNode = */ ff); + return flattenNode(n, /* trivialNode = */ tt, /* skipNode = */ ff); } break; } @@ -160,7 +160,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { 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; } diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 49908c5db..60199c09a 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -17,7 +17,7 @@ #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; diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index d17dd588f..1712509b5 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -24,7 +24,7 @@ #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; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 45946b8c8..6d11364d9 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -19,7 +19,7 @@ #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; diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index a3970c9e3..0eac4c035 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -17,7 +17,7 @@ #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; diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index aeae1073e..cf83150e1 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -167,6 +167,7 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule 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 diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index a2de951aa..ce44b312d 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -25,7 +25,7 @@ #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; diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 67dae0cfa..b51c56b18 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -140,6 +140,15 @@ public: } }; +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) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 686695f98..3c9fd7bd2 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -22,7 +22,7 @@ #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" @@ -1399,4 +1399,4 @@ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { }else{ return NodeManager::currentNM()->mkNode( AND, assumptions ); } -} \ No newline at end of file +} diff --git a/src/theory/decision_attributes.h b/src/theory/decision_attributes.h index 204362a2a..79f58feb1 100644 --- a/src/theory/decision_attributes.h +++ b/src/theory/decision_attributes.h @@ -14,8 +14,10 @@ ** 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" @@ -33,4 +35,4 @@ typedef expr::Attribute Decis }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__DECISION_ATRRIBUTES */ +#endif /* __CVC4__THEORY__DECISION_ATTRIBUTES */ diff --git a/src/theory/model.cpp b/src/theory/model.cpp deleted file mode 100644 index b6ef924d7..000000000 --- a/src/theory/model.cpp +++ /dev/null @@ -1,881 +0,0 @@ -/********************* */ -/*! \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 argTypes = t.getArgTypes(); - vector 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 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().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::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* 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::iterator type_it; - set::iterator i, i2; - bool changed, unassignedAssignable, assignOne = false; - set 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* 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* 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& noRepSet = TypeSet::getSet(it); - if (noRepSet.empty()) { - continue; - } - TypeNode t = TypeSet::getType(it); - TypeNode tb = t.getBaseType(); - if (!assignOne) { - set* 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& 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& noRepSet = TypeSet::getSet(it); - set::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::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 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; isecond.size(); i++ ){ - un = it->second[i]; - vector 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 ); - } - } - } -} diff --git a/src/theory/model.h b/src/theory/model.h deleted file mode 100644 index 8192274b5..000000000 --- a/src/theory/model.h +++ /dev/null @@ -1,283 +0,0 @@ -/********************* */ -/*! \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 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* 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*, TypeNodeHashFunction> TypeSetMap; - typedef std::hash_map 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* s; - if (it == d_typeSet.end()) { - s = new std::set; - d_typeSet[t] = s; - } - else { - s = (*it).second; - } - s->insert(n); - } - - std::set* 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* s; - if (itSet == d_typeSet.end()) { - s = new std::set; - 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& 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 NodeMap; - NodeMap d_normalizedCache; - typedef std::hash_set NodeSet; - - /** process build model */ - virtual void processBuildModel(TheoryModel* m, bool fullModel); - /** normalize representative */ - Node normalize(TheoryModel* m, TNode r, std::map& 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 diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index f6e012660..b5bdff9ee 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -17,7 +17,7 @@ #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 { diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index b96c58767..93cc1205e 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -18,7 +18,7 @@ #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 { diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 1c2c38c51..0c3c74b5f 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -19,7 +19,7 @@ #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" diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 944df63b2..f5724f488 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -13,10 +13,10 @@ ** \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" diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b7576659a..66cc2a434 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -20,7 +20,7 @@ #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" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 93b3f0d7e..af4dea293 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -40,7 +40,8 @@ #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" @@ -1218,7 +1219,7 @@ public: 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 diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp new file mode 100644 index 000000000..73ff068b4 --- /dev/null +++ b/src/theory/theory_model.cpp @@ -0,0 +1,881 @@ +/********************* */ +/*! \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 argTypes = t.getArgTypes(); + vector 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 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().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::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* 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::iterator type_it; + set::iterator i, i2; + bool changed, unassignedAssignable, assignOne = false; + set 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* 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* 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& noRepSet = TypeSet::getSet(it); + if (noRepSet.empty()) { + continue; + } + TypeNode t = TypeSet::getType(it); + TypeNode tb = t.getBaseType(); + if (!assignOne) { + set* 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& 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& noRepSet = TypeSet::getSet(it); + set::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::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 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; isecond.size(); i++ ){ + un = it->second[i]; + vector 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 ); + } + } + } +} diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h new file mode 100644 index 000000000..9da9cb5e2 --- /dev/null +++ b/src/theory/theory_model.h @@ -0,0 +1,282 @@ +/********************* */ +/*! \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 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* 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*, TypeNodeHashFunction> TypeSetMap; + typedef std::hash_map 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* s; + if (it == d_typeSet.end()) { + s = new std::set; + d_typeSet[t] = s; + } + else { + s = (*it).second; + } + s->insert(n); + } + + std::set* 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* s; + if (itSet == d_typeSet.end()) { + s = new std::set; + 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& 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 NodeMap; + NodeMap d_normalizedCache; + typedef std::hash_set NodeSet; + + /** process build model */ + virtual void processBuildModel(TheoryModel* m, bool fullModel); + /** normalize representative */ + Node normalize(TheoryModel* m, TNode r, std::map& 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 */ diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index 326c6c913..6d1a4c9af 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -17,9 +17,10 @@ ** 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" diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 0ee7a2bdd..1045c5a24 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -19,7 +19,7 @@ #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; diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 133cd2cf2..e3ab24efa 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -17,7 +17,7 @@ #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 { diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index dab105d20..052b2f568 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -19,10 +19,9 @@ #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 diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 5b8da8828..2f278625a 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -87,8 +87,8 @@ libutil_la_SOURCES = \ 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 diff --git a/src/util/model.cpp b/src/util/model.cpp new file mode 100644 index 000000000..1d14a7c4f --- /dev/null +++ b/src/util/model.cpp @@ -0,0 +1,52 @@ +/********************* */ +/*! \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 + +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 */ diff --git a/src/util/model.h b/src/util/model.h new file mode 100644 index 000000000..2224f74db --- /dev/null +++ b/src/util/model.h @@ -0,0 +1,78 @@ +/********************* */ +/*! \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 +#include + +#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 */ diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp deleted file mode 100644 index 1c2dc2edf..000000000 --- a/src/util/util_model.cpp +++ /dev/null @@ -1,52 +0,0 @@ -/********************* */ -/*! \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 - -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 */ diff --git a/src/util/util_model.h b/src/util/util_model.h deleted file mode 100644 index e5bd1f955..000000000 --- a/src/util/util_model.h +++ /dev/null @@ -1,78 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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 */