summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp92
1 files changed, 77 insertions, 15 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7a67012a2..6dbabfe4d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -42,6 +42,11 @@
#include "theory/quantifiers/model_engine.h"
#include "theory/quantifiers/first_order_model.h"
+//hack
+#include "theory/arith/options.h"
+#include "theory/uf/options.h"
+
+
using namespace std;
using namespace CVC4;
@@ -85,7 +90,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
d_quantEngine = new QuantifiersEngine(context, this);
//build model information if applicable
- d_curr_model = new theory::DefaultModel( context, "DefaultModel", false );
+ d_curr_model = new theory::DefaultModel( context, "DefaultModel", true );
d_curr_model_builder = new theory::TheoryEngineModelBuilder( this );
Rewriter::init();
@@ -144,33 +149,57 @@ void TheoryEngine::preRegister(TNode preprocessed) {
}
}
+void collectGroundTerms( Node n, std::vector< Node >& defineFuns,
+ std::vector< Node >& groundTerms ){
+ if( std::find( groundTerms.begin(), groundTerms.end(), n )==groundTerms.end() ){
+ groundTerms.push_back( n );
+ if( n.getKind()==kind::APPLY_UF ){
+ if( std::find( defineFuns.begin(), defineFuns.end(), n.getOperator() )==defineFuns.end() ){
+ defineFuns.push_back( n.getOperator() );
+ }
+ }else if( n.getNumChildren()==0 ){
+ if( std::find( defineFuns.begin(), defineFuns.end(), n )==defineFuns.end() ){
+ defineFuns.push_back( n );
+ }
+ }
+ if( n.getKind()==kind::FORALL ){
+ std::cout << "Bad ground assertion : " << n << std::endl;
+ std::cout << "...possible nested quantifiers?" << std::endl;
+ exit( -1 );
+ }
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ collectGroundTerms( n[i], defineFuns, groundTerms );
+ }
+ }
+}
+
void TheoryEngine::printAssertions(const char* tag) {
- if (Debug.isOn(tag)) {
+ if (Trace.isOn(tag)) {
+
for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
Theory* theory = d_theoryTable[theoryId];
if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
- Debug(tag) << "--------------------------------------------" << std::endl;
- Debug(tag) << "Assertions of " << theory->getId() << ": " << std::endl;
+ Trace(tag) << "--------------------------------------------" << std::endl;
+ Trace(tag) << "Assertions of " << theory->getId() << ": " << std::endl;
context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
for (unsigned i = 0; it != it_end; ++ it, ++i) {
if ((*it).isPreregistered) {
- Debug(tag) << "[" << i << "]: ";
+ Trace(tag) << "[" << i << "]: ";
} else {
- Debug(tag) << "(" << i << "): ";
+ Trace(tag) << "(" << i << "): ";
}
- Debug(tag) << (*it).assertion << endl;
+ Trace(tag) << (*it).assertion << endl;
}
if (d_logicInfo.isSharingEnabled()) {
- Debug(tag) << "Shared terms of " << theory->getId() << ": " << std::endl;
+ Trace(tag) << "Shared terms of " << theory->getId() << ": " << std::endl;
context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
for (unsigned i = 0; it != it_end; ++ it, ++i) {
- Debug(tag) << "[" << i << "]: " << (*it) << endl;
+ Trace(tag) << "[" << i << "]: " << (*it) << endl;
}
}
}
}
-
}
}
@@ -312,7 +341,8 @@ void TheoryEngine::check(Theory::Effort effort) {
Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;
- if (Debug.isOn("theory::assertions")) {
+ Trace("theory::assertions") << std::endl;
+ if (Trace.isOn("theory::assertions")) {
printAssertions("theory::assertions");
}
@@ -346,7 +376,8 @@ void TheoryEngine::check(Theory::Effort effort) {
! d_inConflict &&
! d_lemmasAdded ) {
if( d_logicInfo.isQuantified() ){
- ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->performCheck(Theory::EFFORT_LAST_CALL);
+ //quantifiers engine must pass effort last call check
+ d_quantEngine->check(Theory::EFFORT_LAST_CALL);
// if we have given up, then possibly flip decision
if(options::flipDecision()) {
if(d_incomplete && !d_inConflict && !d_lemmasAdded) {
@@ -358,7 +389,7 @@ void TheoryEngine::check(Theory::Effort effort) {
//if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
}else if( options::produceModels() ){
//must build model at this point
- d_curr_model_builder->buildModel( d_curr_model );
+ d_curr_model_builder->buildModel( d_curr_model, true );
}
}
@@ -436,6 +467,7 @@ void TheoryEngine::combineTheories() {
d_factsAsserted = true;
continue;
} else {
+ Message() << "mark propagation fail: " << literal << " " << normalizedLiteral << " " << carePair.theory << std::endl;
Unreachable();
}
}
@@ -560,12 +592,14 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
return true;
}
-void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){
+void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
+ //have shared term engine collectModelInfo
+ d_sharedTerms.collectModelInfo( m, fullModel );
// Consult each active theory to get all relevant information
// concerning the model.
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
if(d_logicInfo.isTheoryEnabled(theoryId)) {
- d_theoryTable[theoryId]->collectModelInfo(m);
+ d_theoryTable[theoryId]->collectModelInfo( m, fullModel );
}
}
}
@@ -688,6 +722,16 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut);
Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
+ //must add substitutions to model
+ theory::TheoryModel* m = getModel();
+ if( m ){
+ for( SubstitutionMap::iterator pos = substitutionOut.begin(); pos != substitutionOut.end(); ++pos) {
+ Node n = (*pos).first;
+ Node v = (*pos).second;
+ Trace("model") << "Add substitution : " << n << " " << v << std::endl;
+ m->addSubstitution( n, v );
+ }
+ }
return solveStatus;
}
@@ -1307,3 +1351,21 @@ void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
{
d_unconstrainedSimp.processAssertions(assertions);
}
+
+
+void TheoryEngine::setUserAttribute( std::string& attr, Node n ){
+ Trace("te-attr") << "set user attribute " << attr << " " << n << std::endl;
+ if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
+ for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
+ d_attr_handle[attr][i]->setUserAttribute( attr, n );
+ }
+ }else{
+ //unhandled exception?
+ }
+}
+
+void TheoryEngine::handleUserAttribute( const char* attr, Theory* t ){
+ Trace("te-attr") << "Handle user attribute " << attr << " " << t << std::endl;
+ std::string str( attr );
+ d_attr_handle[ str ].push_back( t );
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback