theory/quantifiers/quant_conflict_find.cpp \
theory/quantifiers/conjecture_generator.h \
theory/quantifiers/conjecture_generator.cpp \
+ theory/quantifiers/ce_guided_instantiation.h \
+ theory/quantifiers/ce_guided_instantiation.cpp \
theory/quantifiers/options_handlers.h \
theory/arith/theory_arith_type_rules.h \
theory/arith/type_enumerator.h \
PARSER_STATE->warning(ss.str());
}
// do nothing
- } else if(attr == ":axiom" || attr == ":conjecture") {
+ } else if(attr==":axiom" || attr==":conjecture" || attr==":sygus" || attr==":synthesis") {
if(hasValue) {
std::stringstream ss;
ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
--- /dev/null
+/********************* */
+/*! \file ce_guided_instantiation.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief counterexample guided instantiation class
+ **
+ **/
+
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) {
+
+
+}
+
+void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
+ //TODO
+}
+
+void CegInstantiation::registerQuantifier( Node q ) {
+ //TODO
+}
+
+void CegInstantiation::assertNode( Node n ) {
+
+}
+
+}
\ No newline at end of file
--- /dev/null
+/********************* */
+/*! \file ce_guided_instantiation.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief counterexample guided instantiation class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CE_GUIDED_INSTANTIATION_H
+#define CE_GUIDED_INSTANTIATION_H
+
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class CegInstantiation : public QuantifiersModule
+{
+public:
+ CegInstantiation( QuantifiersEngine * qe, context::Context* c );
+public:
+ /* Call during quantifier engine's check */
+ void check( Theory::Effort e, unsigned quant_e );
+ /* Called for new quantifiers */
+ void registerQuantifier( Node q );
+ void assertNode( Node n );
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ std::string identify() const { return "CegInstantiation"; }
+};
+
+}
+}
+}
+
+#endif
Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
return mkRationalNode(qmodel);
}
-
-
-InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :
- InstStrategy( qe ), d_th( th ){
-
-}
-
-bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){
- //DO_THIS
- return false;
-}
-
-void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
- Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
- if( e<2 ){
- return InstStrategy::STATUS_UNFINISHED;
- }else if( e==2 ){
- InstMatch m( f );
- for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
- Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
- if( i.getType().isDatatype() ){
- Node n = getValueFor( i );
- Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
- m.setValue( j, n);
- }
- }
- //d_quantEngine->addInstantiation( f, m );
- }
- return InstStrategy::STATUS_UNKNOWN;
-}
-
-Node InstStrategyDatatypesValue::getValueFor( Node n ){
- //simply get the ground value for n in the current model, if it exists,
- // or return an arbitrary ground term otherwise
- if( !TermDb::hasInstConstAttr(n) ){
- return n;
- }else{
- return n;
- }
-}
};
-class InstStrategyDatatypesValue : public InstStrategy
-{
-protected:
- /** calculate if we should process this quantifier */
- bool calculateShouldProcess( Node f );
-private:
- /** reference to theory datatypes */
- datatypes::TheoryDatatypes* d_th;
- /** get value function */
- Node getValueFor( Node n );
-public:
- //constructor
- InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );
- ~InstStrategyDatatypesValue(){}
- /** reset instantiation */
- void processResetInstantiationRound( Theory::Effort effort );
- /** process method, returns a status */
- int process( Node f, Theory::Effort effort, int e );
- /** identify */
- std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
-
-};/* class InstStrategy */
-
}
}
}
for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
- if( TermDb::isRewriteRule( n ) ){
+ if( !d_quantEngine->hasOwnership( n, this ) ){
d_quant_active[n] = false;
}else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){
d_quant_active[n] = false;
}
void InstantiationEngine::registerQuantifier( Node f ){
- if( !TermDb::isRewriteRule( f ) ){
+ if( d_quantEngine->hasOwnership( f, this ) ){
//Notice() << "do cbqi " << f << " ? " << std::endl;
if( options::cbqi() ){
Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
}
bool QModelBuilder::isQuantifierActive( Node f ) {
- return !TermDb::isRewriteRule( f );
+ return d_qe->hasOwnership( f );
}
}
bool QModelBuilderIG::isQuantifierActive( Node f ){
- return !TermDb::isRewriteRule( f ) &&
- ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end();
+ return d_qe->hasOwnership( f ) && ( d_considerAxioms || !d_qe->getTermDatabase()->isQAttrAxiom( f ) ) && d_quant_sat.find( f )==d_quant_sat.end();
}
bool QModelBuilderIG::isTermActive( Node n ){
number of ground terms to generate for model filtering
option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
more aggressive merging for universal equality engine, introduces terms
+
+option ceGuidedInst --cegqi bool :default false
+ counterexample guided quantifier instantiation
+
endmodule
//-------------------------------------------------- registration\r
\r
void QuantConflictFind::registerQuantifier( Node q ) {\r
- if( !TermDb::isRewriteRule( q ) ){\r
+ if( d_quantEngine->hasOwnership( q, this ) ){\r
d_quants.push_back( q );\r
d_quant_id[q] = d_quants.size();\r
Trace("qcf-qregister") << "Register ";\r
//-------------------------------------------------- handling assertions / eqc\r
\r
void QuantConflictFind::assertNode( Node q ) {\r
- if( !TermDb::isRewriteRule( q ) ){\r
+ if( d_quantEngine->hasOwnership( q, this ) ){\r
Trace("qcf-proc") << "QCF : assertQuantifier : ";\r
debugPrintQuant("qcf-proc", q);\r
Trace("qcf-proc") << std::endl;\r
Trace("quant-attr-debug") << "Set conjecture " << n << std::endl;
ConjectureAttribute ca;
n.setAttribute( ca, true );
+ }else if( attr=="sygus" ){
+ Trace("quant-attr-debug") << "Set sygus " << n << std::endl;
+ SygusAttribute ca;
+ n.setAttribute( ca, true );
+ }else if( attr=="synthesis" ){
+ Trace("quant-attr-debug") << "Set synthesis " << n << std::endl;
+ SynthesisAttribute ca;
+ n.setAttribute( ca, true );
}else if( attr=="quant-inst-max-level" ){
Assert( node_values.size()==1 );
uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
NodeBuilder<> patternListB(kind::INST_PATTERN_LIST);
//the entire rewrite rule is the first pattern
if( options::quantRewriteRules() ){
- patternListB << NodeManager::currentNM()->mkNode( INST_PATTERN, r );
+ patternListB << NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, r );
}
patternListB << static_cast<Node>(patternB);
forallB << static_cast<Node>(patternListB);
#include "theory/quantifiers/theory_quantifiers.h"
#include "util/datatype.h"
#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
+#include "theory/quantifiers/rewrite_engine.h"
using namespace std;
using namespace CVC4;
Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
d_qattr_conjecture[q] = true;
}
+ if( avar.getAttribute(SygusAttribute()) ){
+ Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
+ d_qattr_sygus[q] = true;
+ d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+ }
+ if( avar.getAttribute(SynthesisAttribute()) ){
+ Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
+ d_qattr_synthesis[q] = true;
+ d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation() );
+ }
if( avar.hasAttribute(QuantInstLevelAttribute()) ){
d_qattr_qinstLevel[q] = avar.getAttribute(QuantInstLevelAttribute());
Trace("quant-attr") << "Attribute : quant inst level " << d_qattr_qinstLevel[q] << " : " << q << std::endl;
d_qattr_rr_priority[q] = avar.getAttribute(RrPriorityAttribute());
Trace("quant-attr") << "Attribute : rr priority " << d_qattr_rr_priority[q] << " : " << q << std::endl;
}
+ if( avar.getKind()==REWRITE_RULE ){
+ Assert( i==0 );
+ //set rewrite engine as owner
+ d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine() );
+ }
}
}
}
}
}
+bool TermDb::isQAttrSygus( Node q ) {
+ std::map< Node, bool >::iterator it = d_qattr_sygus.find( q );
+ if( it==d_qattr_sygus.end() ){
+ return false;
+ }else{
+ return it->second;
+ }
+}
+
+bool TermDb::isQAttrSynthesis( Node q ) {
+ std::map< Node, bool >::iterator it = d_qattr_synthesis.find( q );
+ if( it==d_qattr_synthesis.end() ){
+ return false;
+ }else{
+ return it->second;
+ }
+}
+
int TermDb::getQAttrQuantInstLevel( Node q ) {
std::map< Node, int >::iterator it = d_qattr_qinstLevel.find( q );
if( it==d_qattr_qinstLevel.end() ){
struct ConjectureAttributeId {};
typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
+/** Attribute true for quantifiers that are SyGus conjectures */
+struct SygusAttributeId {};
+typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
+
+/** Attribute true for quantifiers that are synthesis conjectures */
+struct SynthesisAttributeId {};
+typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
+
/** Attribute true for nodes that should not be used for matching */
struct NoMatchAttributeId {};
/** use the special for boolean flag */
private:
std::map< Node, bool > d_qattr_conjecture;
std::map< Node, bool > d_qattr_axiom;
+ std::map< Node, bool > d_qattr_sygus;
+ std::map< Node, bool > d_qattr_synthesis;
std::map< Node, int > d_qattr_rr_priority;
std::map< Node, int > d_qattr_qinstLevel;
//record attributes
bool isQAttrConjecture( Node q );
/** is axiom */
bool isQAttrAxiom( Node q );
+ /** is sygus conjecture */
+ bool isQAttrSygus( Node q );
+ /** is synthesis conjecture */
+ bool isQAttrSynthesis( Node q );
/** get instantiation level */
int getQAttrQuantInstLevel( Node q );
/** get rewrite rule priority */
#include "theory/quantifiers/rewrite_engine.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/conjecture_generator.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/uf/options.h"
#include "theory/uf/theory_uf.h"
}else{
d_rr_engine = NULL;
}
+ if( options::ceGuidedInst() ){
+ d_ceg_inst = new quantifiers::CegInstantiation( this, c );
+ d_modules.push_back( d_ceg_inst );
+ }else{
+ d_ceg_inst = NULL;
+ }
//options
d_total_inst_count_debug = 0;
}
}
+QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
+ std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
+ if( it==d_owner.end() ){
+ return NULL;
+ }else{
+ return it->second;
+ }
+}
+
+void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) {
+ QuantifiersModule * mo = getOwner( q );
+ if( mo!=m ){
+ if( mo!=NULL ){
+ Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << m->identify() << ", but already has owner " << mo->identify() << "!" << std::endl;
+ }
+ d_owner[q] = m;
+ }
+}
+
+bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
+ QuantifiersModule * mo = getOwner( q );
+ return mo==m || mo==NULL;
+}
+
void QuantifiersEngine::check( Theory::Effort e ){
CodeTimer codeTimer(d_time);
bool needsCheck = false;
void QuantifiersEngine::registerQuantifier( Node f ){
if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
Trace("quant") << "QuantifiersEngine : Register quantifier ";
- if( d_term_db->isRewriteRule( f ) ){
- Trace("quant") << " (rewrite rule)";
- }
Trace("quant") << " : " << f << std::endl;
d_quants.push_back( f );
//make instantiation constants for f
d_term_db->makeInstantiationConstantsFor( f );
d_term_db->computeAttributes( f );
+ QuantifiersModule * qm = getOwner( f );
+ if( qm!=NULL ){
+ Trace("quant") << " Owner : " << qm->identify() << std::endl;
+ }
//register with quantifier relevance
if( d_quant_rel ){
d_quant_rel->registerQuantifier( f );
class RewriteEngine;
class RelevantDomain;
class ConjectureGenerator;
+ class CegInstantiation;
}/* CVC4::theory::quantifiers */
namespace inst {
quantifiers::RewriteEngine * d_rr_engine;
/** subgoal generator */
quantifiers::ConjectureGenerator * d_sg_gen;
+ /** ceg instantiation */
+ quantifiers::CegInstantiation * d_ceg_inst;
public: //effort levels
enum {
QEFFORT_CONFLICT,
/** get equality query object for the given type. The default is the
generic one */
EqualityQueryQuantifiersEngine* getEqualityQuery();
- /** get instantiation engine */
- quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
- /** get model engine */
- quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
/** get default sat context for quantifiers engine */
context::Context* getSatContext();
/** get default sat context for quantifiers engine */
QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
/** get phase requirement terms */
void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
+public: //modules
+ /** get instantiation engine */
+ quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
+ /** get model engine */
+ quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
/** get bounded integers utility */
quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
/** Conflict find mechanism for quantifiers */
quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
+ /** rewrite rules utility */
+ quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; }
+ /** subgoal generator */
+ quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
+ /** ceg instantiation */
+ quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
+private:
+ /** owner of quantified formulas */
+ std::map< Node, QuantifiersModule * > d_owner;
+public:
+ /** get owner */
+ QuantifiersModule * getOwner( Node q );
+ /** set owner */
+ void setOwner( Node q, QuantifiersModule * m );
+ /** considers */
+ bool hasOwnership( Node q, QuantifiersModule * m = NULL );
public:
/** initialize */
void finishInit();
projects / cvc5.git / commitdiff