{
restrictions.d_iteReturnBoolConst = true;
}
+ // register the strategy
+ registerStrategy(f, enums, restrictions.d_unused_strategies);
d_strategy[f].staticLearnRedundantOps(strategy_lemmas, restrictions);
- registerStrategy(f, enums);
// Copy candidates and check whether CegisUnif for any of them
if (d_unif_candidates.find(f) != d_unif_candidates.end())
{
return it->second;
}
-void SygusUnifRl::registerStrategy(Node f, std::vector<Node>& enums)
+void SygusUnifRl::registerStrategy(
+ Node f,
+ std::vector<Node>& enums,
+ std::map<Node, std::unordered_set<unsigned>>& unused_strats)
{
if (Trace.isOn("sygus-unif-rl-strat"))
{
Trace("sygus-unif-rl-strat") << "Register..." << std::endl;
Node e = d_strategy[f].getRootEnumerator();
std::map<Node, std::map<NodeRole, bool>> visited;
- registerStrategyNode(f, e, role_equal, visited, enums);
+ registerStrategyNode(f, e, role_equal, visited, enums, unused_strats);
}
void SygusUnifRl::registerStrategyNode(
Node e,
NodeRole nrole,
std::map<Node, std::map<NodeRole, bool>>& visited,
- std::vector<Node>& enums)
+ std::vector<Node>& enums,
+ std::map<Node, std::unordered_set<unsigned>>& unused_strats)
{
Trace("sygus-unif-rl-strat") << " register node " << e << std::endl;
if (visited[e].find(nrole) != visited[e].end())
EnumTypeInfoStrat* etis = snode.d_strats[j];
StrategyType strat = etis->d_this;
// is this a simple recursive ITE strategy?
+ bool success = false;
if (strat == strat_ITE && nrole == role_equal)
{
- bool success = true;
+ success = true;
for (unsigned c = 1; c <= 2; c++)
{
std::pair<Node, NodeRole> child = etis->d_cenum[c];
enums.push_back(e);
}
}
+ if (!success)
+ {
+ unused_strats[e].insert(j);
+ }
// TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
}
}
*
* Initialize the above data for the relevant enumerators in the strategy tree
* of candidate variable f. For each strategy point e which there is a
- * decision tree strategy, we add e to enums.
+ * decision tree strategy, we add e to enums. For each strategy with index
+ * i in an strategy point e, if we are not using the strategy, we add i to
+ * unused_strats[e]. This map is later passed to
+ * SygusUnifStrategy::staticLearnRedundantOps.
*/
- void registerStrategy(Node f, std::vector<Node>& enums);
+ void registerStrategy(
+ Node f,
+ std::vector<Node>& enums,
+ std::map<Node, std::unordered_set<unsigned>>& unused_strats);
/** register strategy node
*
* Called while traversing the strategy tree of f. The arguments e and nrole
* indicate the current node in the tree we are traversing, and visited
- * indicates the nodes we have already visited. If e has a decision tree
- * strategy, it is added to enums.
+ * indicates the nodes we have already visited. The arguments enums and
+ * unused_strats are modified as described above.
*/
- void registerStrategyNode(Node f,
- Node e,
- NodeRole nrole,
- std::map<Node, std::map<NodeRole, bool>>& visited,
- std::vector<Node>& enums);
+ void registerStrategyNode(
+ Node f,
+ Node e,
+ NodeRole nrole,
+ std::map<Node, std::map<NodeRole, bool>>& visited,
+ std::vector<Node>& enums,
+ std::map<Node, std::unordered_set<unsigned>>& unused_strats);
/** register conditional enumerator
*
* Registers that cond is a conditional enumerator for building a (recursive)
TypeNode etn = e.getType();
EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
StrategyNode& snode = tinfo.getStrategyNode(nrole);
+ // the constructors of the current strategy point we need
std::map<unsigned, bool> needs_cons_curr;
- // constructors that correspond to strategies are not needed
- // the intuition is that the strategy itself is responsible for constructing
- // all terms that use the given constructor
+ // get the unused strategies
+ std::map<Node, std::unordered_set<unsigned>>::iterator itus =
+ restrictions.d_unused_strategies.find(e);
+ std::unordered_set<unsigned> unused_strats;
+ if (itus != restrictions.d_unused_strategies.end())
+ {
+ unused_strats.insert(itus->second.begin(), itus->second.end());
+ }
for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
{
+ // if we are not using this strategy, there is nothing to do
+ if (unused_strats.find(j) != unused_strats.end())
+ {
+ continue;
+ }
EnumTypeInfoStrat* etis = snode.d_strats[j];
unsigned cindex =
static_cast<unsigned>(Datatype::indexOf(etis->d_cons.toExpr()));
+ // constructors that correspond to strategies are not needed
+ // the intuition is that the strategy itself is responsible for constructing
+ // all terms that use the given constructor
Trace("sygus-strat-slearn") << "...by strategy, can exclude operator "
<< etis->d_cons << std::endl;
needs_cons_curr[cindex] = false;
* the condition values of ITEs to be restricted to atoms
*/
bool d_iteCondOnlyAtoms;
+ /**
+ * A list of unused strategies. This maps strategy points to the indices
+ * in StrategyNode::d_strats that are not used by the caller of
+ * staticLearnRedundantOps, and hence should not be taken into account
+ * when doing redundant operator learning.
+ */
+ std::map<Node, std::unordered_set<unsigned>> d_unused_strategies;
};
/**
regress1/sygus/no-flat-simp.sy \
regress1/sygus/no-mention.sy \
regress1/sygus/pbe_multi.sy \
+ regress1/sygus/planning-unif.sy \
regress1/sygus/process-10-vars.sy \
regress1/sygus/qe.sy \
regress1/sygus/real-grammar.sy \
--- /dev/null
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-unif --sygus-out=status
+(set-logic LIA)
+
+(define-fun get-y ((currPoint Int)) Int
+(ite (< currPoint 10) 0 (ite (< currPoint 20) 1 (ite (< currPoint 30) 2 (ite (< currPoint 40) 3 (ite (< currPoint 50) 4 (ite (< currPoint 60) 5 (ite (< currPoint 70) 6 (ite (< currPoint 80) 7 (ite (< currPoint 90) 8 9))))))))))
+
+(define-fun get-x ((currPoint Int)) Int
+ (- currPoint (* (get-y currPoint) 10)))
+(define-fun interpret-move (( currPoint Int ) ( move Int)) Int
+(ite (= move 0) currPoint
+(ite (= move 1) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10))
+(ite (= move 2) (ite (or (< (+ (get-x currPoint) 1) 0) (>= (+ (get-x currPoint) 1) 10)) currPoint (+ currPoint 1))
+(ite (= move 3) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10))
+(ite (= move 4) (ite (or (< (+ (get-x currPoint) -1) 0) (>= (+ (get-x currPoint) -1) 10)) currPoint (+ currPoint -1))
+currPoint))))))
+
+(define-fun interpret-move-obstacle-0 (( currPoint Int ) ( move Int)) Int
+(ite (= move 0) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10))
+(ite (= move 1) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10))
+currPoint)))
+
+(define-fun interpret-move-obstacle-1 (( currPoint Int ) ( move Int)) Int
+(ite (= move 0) (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10)) currPoint (+ currPoint 10))
+(ite (= move 1) currPoint
+(ite (= move 2) (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10)) currPoint (+ currPoint -10))
+currPoint))))
+
+(define-fun allowable-move-obstacle-0 (( start Int ) ( end Int)) Bool
+ (or (= (interpret-move-obstacle-0 start 0) end)
+ (or (= (interpret-move-obstacle-0 start 1) end) false)))
+
+(define-fun allowable-move-obstacle-1 (( start Int ) ( end Int)) Bool
+ (or (= (interpret-move-obstacle-1 start 0) end)
+ (or (= (interpret-move-obstacle-1 start 1) end)
+ (or (= (interpret-move-obstacle-1 start 2) end) false))))
+
+(define-fun get-move-obstacle-0 (( start Int ) ( end Int)) Int
+ (ite (= (interpret-move-obstacle-0 start 0) end) 0
+ (ite (= (interpret-move-obstacle-0 start 1) end) 1 -1)))
+
+(define-fun get-move-obstacle-1 (( start Int ) ( end Int)) Int
+ (ite (= (interpret-move-obstacle-1 start 0) end) 0
+ (ite (= (interpret-move-obstacle-1 start 1) end) 1
+ (ite (= (interpret-move-obstacle-1 start 2) end) 2 -1))))
+
+(define-fun no-overlap-one-move-combination-2-2 ((p0 Int) (p1 Int) (p2 Int) (p3 Int)) Bool
+ (and (not (= p0 p2)) (and (not (= p0 p3)) (and (not (= p1 p2)) (and (not (= p1 p3)) true)))))
+
+(define-fun no-overlaps-0 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool
+ (= 1
+ (ite (= move 0)
+ (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+ (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+ (ite (= move 1)
+ (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+ (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+ (ite (= move 2)
+ (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+ (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+ (ite (= move 3)
+ (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+ (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+ (ite (= move 4)
+ (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+ (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) 0)))))))
+
+(define-fun no-overlaps-1 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool
+ (= 1
+ (ite (= move 0)
+ (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+ (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+ (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+ (ite (= move 1)
+ (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+ (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+ (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+ (ite (= move 2)
+ (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+ (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+ (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+ (ite (= move 3)
+ (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+ (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+ (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+ (ite (= move 4)
+ (ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+ (ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+ (ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) 0)))))))
+
+(define-fun no-overlaps-one-step-helper ((currPoint Int) (move Int) (o0-t Int) (o0move Int) (o1-t Int) (o1move Int)) Bool
+ (and (no-overlaps-0 currPoint move o0-t o0move) (and (no-overlaps-1 currPoint move o1-t o1move) true)))
+
+(define-fun no-overlaps-one-step ((currPoint Int) (move Int) (o0-0 Int) (o0-1 Int) (o1-0 Int) (o1-1 Int)) Bool
+ (no-overlaps-one-step-helper currPoint move o0-0 (get-move-obstacle-0 o0-0 o0-1) o1-0 (get-move-obstacle-1 o1-0 o1-1)))
+
+
+
+(declare-var o0-1 Int)
+(declare-var o0-2 Int)
+(declare-var o0-3 Int)
+(declare-var o1-1 Int)
+(declare-var o1-2 Int)
+(declare-var o1-3 Int)
+
+(synth-fun move ((currPoint Int) (o0 Int) (o1 Int)) Int
+ ((Start Int (
+ MoveId
+ (ite StartBool Start Start)))
+ (MoveId Int (0
+ 1
+ 2
+ 3
+ 4
+ ))
+ (CondInt Int (
+ (get-y currPoint) ;y coord
+ (get-x currPoint) ;x coord
+ (get-y o0)
+ (get-x o0)
+ (get-y o1)
+ (get-x o1)
+ (+ CondInt CondInt)
+ (- CondInt CondInt)
+ -1
+ 0
+ 1
+ 2
+ 3
+ 4
+ 5
+ 6
+ 7
+ 8
+ 9
+ ))
+ (StartBool Bool ((and StartBool StartBool)
+ (or StartBool StartBool)
+ (not StartBool)
+ (<= CondInt CondInt)
+ (= CondInt CondInt)
+ (>= CondInt CondInt)))))
+
+ (constraint (or
+ (and
+ (= (interpret-move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) (move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) o0-2 o1-2)) 30)
+ (and (no-overlaps-one-step 0 (move 0 99 98) 99 o0-1 98 o1-1) (and (no-overlaps-one-step (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1) o0-1 o0-2 o1-1 o1-2) (and (no-overlaps-one-step (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) (move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) o0-2 o1-2) o0-2 o0-3 o1-2 o1-3) true))))
+ (not (and (allowable-move-obstacle-0 99 o0-1) (and (allowable-move-obstacle-0 o0-1 o0-2) (and (allowable-move-obstacle-0 o0-2 o0-3) (and (allowable-move-obstacle-1 98 o1-1) (and (allowable-move-obstacle-1 o1-1 o1-2) (and (allowable-move-obstacle-1 o1-2 o1-3) true)))))))))
+(check-synth)
projects / cvc5.git / commitdiff