-
-class QIntDef;
-class QuantVarOrder;
-class FirstOrderModelQInt : public FirstOrderModel
-{
- friend class QIntervalBuilder;
-private:
- /** uf op to some representation */
- std::map<Node, QIntDef * > d_models;
- /** representatives to ids */
- std::map< Node, int > d_rep_id;
- std::map< TypeNode, Node > d_min;
- std::map< TypeNode, Node > d_max;
- /** quantifiers to information regarding variable ordering */
- std::map<Node, QuantVarOrder * > d_var_order;
- /** get current model value */
- Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
- void processInitializeModelForTerm(Node n);
-public:
- FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name);
- FirstOrderModelQInt * asFirstOrderModelQInt() { return this; }
- void processInitialize( bool ispre );
- Node getFunctionValue(Node op, const char* argPrefix );
-
- Node getUsedRepresentative( Node n );
- int getRepId( Node n ) { return d_rep_id.find( n )==d_rep_id.end() ? -1 : d_rep_id[n]; }
- bool isLessThan( Node v1, Node v2 );
- Node getMin( Node v1, Node v2 );
- Node getMax( Node v1, Node v2 );
- Node getMinimum( TypeNode tn ) { return getNext( tn, Node::null() ); }
- Node getMaximum( TypeNode tn );
- bool isMinimum( Node n ) { return n==getMinimum( n.getType() ); }
- bool isMaximum( Node n ) { return n==getMaximum( n.getType() ); }
- Node getNext( TypeNode tn, Node v );
- Node getPrev( TypeNode tn, Node v );
- bool doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur );
- QuantVarOrder * getVarOrder( Node q ) { return d_var_order[q]; }
-
- void processInitializeQuantifier( Node q ) ;
- unsigned getOrderedNumVars( Node q );
- TypeNode getOrderedVarType( Node q, int i );
- int getOrderedVarNumToVarNum( Node q, int i );
-};/* class FirstOrderModelQInt */
-
-class AbsDef;
-
-class FirstOrderModelAbs : public FirstOrderModel
-{
-public:
- std::map< Node, AbsDef * > d_models;
- std::map< Node, bool > d_models_valid;
- std::map< TNode, unsigned > d_rep_id;
- std::map< TypeNode, unsigned > d_domain;
- std::map< Node, std::vector< int > > d_var_order;
- std::map< Node, std::map< int, int > > d_var_index;
-private:
- /** get current model value */
- Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
- void processInitializeModelForTerm(Node n);
- void processInitializeQuantifier( Node q );
- void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
-public:
- FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
- FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
- void processInitialize( bool ispre );
- unsigned getRepresentativeId( TNode n );
- TNode getUsedRepresentative( TNode n );
- bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
- Node getFunctionValue(Node op, const char* argPrefix );
- Node getVariable( Node q, unsigned i );
-};
-