Home
last modified time | relevance | path

Searched refs:skolems (Results 1 – 25 of 26) sorted by relevance

12

/dports/devel/hs-hls-install/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/test/
H A DUnificationSpec.hs30 let (skolems, take n -> univars)
36 for (zip skolems univars) randomSwap
41 counterexample (show skolems) $
45 (S.fromList $ mapMaybe tcGetTyVar_maybe skolems)
52 zip univars skolems <&> \(uni, skolem) ->
/dports/devel/hs-haskell-language-server/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/test/
H A DUnificationSpec.hs30 let (skolems, take n -> univars)
36 for (zip skolems univars) randomSwap
41 counterexample (show skolems) $
45 (S.fromList $ mapMaybe tcGetTyVar_maybe skolems)
52 zip univars skolems <&> \(uni, skolem) ->
/dports/math/cvc4/CVC4-1.7/test/unit/expr/
H A Dnode_black.h40 std::vector<Node> skolems; in makeNSkolemNodes() local
45 return skolems; in makeNSkolemNodes()
665 const std::vector<Node> skolems = in testForEachOverNodeAsNodes() local
667 Node add = d_nodeManager->mkNode(kind::PLUS, skolems); in testForEachOverNodeAsNodes()
672 TS_ASSERT(children.size() == skolems.size() && in testForEachOverNodeAsNodes()
677 const std::vector<Node> skolems = in testForEachOverNodeAsTNodes() local
684 TS_ASSERT(children.size() == skolems.size() && in testForEachOverNodeAsTNodes()
689 const std::vector<Node> skolems = in testForEachOverTNodeAsNode() local
697 TS_ASSERT(children.size() == skolems.size() && in testForEachOverTNodeAsNode()
702 const std::vector<Node> skolems = in testForEachOverTNodeAsTNodes() local
[all …]
/dports/devel/hs-hls-install/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/src/Wingman/Judgements/
H A DTheta.hs85 mkSubst skolems a b =
91 skolems' = skolems S.\\ tyvars function
109 allEvidenceToSubst skolems ((a, b) : evs) =
110 let subst = mkSubst skolems a b
112 $ allEvidenceToSubst skolems
/dports/devel/hs-haskell-language-server/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/src/Wingman/Judgements/
H A DTheta.hs85 mkSubst skolems a b =
91 skolems' = skolems S.\\ tyvars function
109 allEvidenceToSubst skolems ((a, b) : evs) =
110 let subst = mkSubst skolems a b
112 $ allEvidenceToSubst skolems
/dports/devel/hs-hls-install/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/src/Wingman/
H A DMachinery.hs97 let skolems = S.fromList function
106 { ts_skolems = skolems
247 skolems <- gets ts_skolems
248 case tryUnifyUnivarsButNotSkolems skolems goal inst of
265 skolems <- gets ts_skolems
266 case tryUnifyUnivarsButNotSkolems skolems goal inst of
287 skolems <- gets ts_skolems
289 case S.size $ vars S.\\ skolems of
H A DAuto.hs20 skolems <- gets ts_skolems
25 traceMX "skolems" skolems
H A DGHC.hs389 tryUnifyUnivarsButNotSkolems skolems goal inst =
391 (bool BindMe Skolem . flip S.member skolems)
/dports/devel/hs-haskell-language-server/haskell-language-server-1.4.0/plugins/hls-tactics-plugin/src/Wingman/
H A DMachinery.hs97 let skolems = S.fromList function
106 { ts_skolems = skolems
247 skolems <- gets ts_skolems
248 case tryUnifyUnivarsButNotSkolems skolems goal inst of
265 skolems <- gets ts_skolems
266 case tryUnifyUnivarsButNotSkolems skolems goal inst of
287 skolems <- gets ts_skolems
289 case S.size $ vars S.\\ skolems of
H A DAuto.hs20 skolems <- gets ts_skolems
25 traceMX "skolems" skolems
H A DGHC.hs389 tryUnifyUnivarsButNotSkolems skolems goal inst =
391 (bool BindMe Skolem . flip S.member skolems)
/dports/math/cvc3/cvc3-2.4.1/src/search/
H A Dsearch_theorem_producer.h41 const ExprMap<bool>& skolems);
43 const ExprMap<bool>& skolems);
H A Dsearch_theorem_producer.cpp413 const ExprMap<bool>& skolems) in checkSoundNoSkolems() argument
419 CHECK_SOUND(skolems.count(e) == 0, in checkSoundNoSkolems()
423 checkSoundNoSkolems(*it, visited, skolems); in checkSoundNoSkolems()
425 checkSoundNoSkolems(e.getBody(), visited, skolems); in checkSoundNoSkolems()
431 const ExprMap<bool>& skolems) in checkSoundNoSkolems() argument
437 checkSoundNoSkolems(t.getExpr(), visited, skolems); in checkSoundNoSkolems()
443 checkSoundNoSkolems(*it, visited, skolems); in checkSoundNoSkolems()
468 ExprMap<bool> skolems; in eliminateSkolemAxioms() local
484 skolems[sk_var] = true; in eliminateSkolemAxioms()
489 checkSoundNoSkolems(tFalse, visited, skolems); in eliminateSkolemAxioms()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dskolemize.cpp50 bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems) in getSkolemConstants() argument
56 skolems.insert(skolems.end(), it->second.begin(), it->second.end()); in getSkolemConstants()
H A Dskolemize.h74 bool getSkolemConstants(Node q, std::vector<Node>& skolems);
H A Dconjecture_generator.cpp585 std::vector<Node> skolems; in check() local
586 d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems); in check()
589 for (unsigned j = 0; j < skolems.size(); j++) in check()
591 TNode k = skolems[j]; in check()
599 for (unsigned k = 0; k < skolems.size(); k++) in check()
601 Trace("sg-conjecture") << skolems[k] << (j == k ? "*" : "") in check()
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/sets/jan28/
H A DTalkingAboutSets.hs.fqout.3577minimized.smt28 ; skolems due to the "two sets not being equal" axiom.
/dports/math/cvc4/CVC4-1.7/src/theory/bv/
H A Dbv_subtheory_algebraic.cpp860 std::vector<Node> skolems; in skolemize() local
867 skolems.push_back(sk); in skolemize()
874 skolems.push_back(sk); in skolemize()
878 for (int i = skolems.size() - 1; i >= 0; --i) { in skolemize()
879 skolem_nb << skolems[i]; in skolemize()
882 Node skolem_concat = skolems.size() == 1 ? (Node)skolems[0] : (Node) skolem_nb; in skolemize()
H A Dabstraction.cpp287 vector<Node>& skolems = d_signatureSkolems[bitwidth]; in getSignatureSkolem() local
290 Assert(skolems.size() + 1 >= index); in getSignatureSkolem()
291 if (skolems.size() == index) in getSignatureSkolem()
295 skolems.push_back(nm->mkSkolem(os.str(), in getSignatureSkolem()
300 return skolems[index]; in getSignatureSkolem()
/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dtheory_uf.cpp760 std::vector< Node > skolems; in getExtensionalityDeq() local
766 skolems.push_back( k ); in getExtensionalityDeq()
779 children.insert( children.end(), skolems.begin(), skolems.end() ); in getExtensionalityDeq()
/dports/textproc/py-rdflib/rdflib-5.0.0/rdflib/
H A Dterm.py72 skolems = {} variable
309 if bnode_id in skolems:
310 return skolems[bnode_id]
313 skolems[bnode_id] = retval
/dports/lang/purescript/purescript-0.14.5/src/Language/PureScript/TypeChecker/Entailment/
H A DCoercible.hs387 go (ConstrainedType sa Constraint{..} ty) | s1 `S.notMember` foldMap skolems constraintArgs =
464 skolems :: SourceType -> S.Set Int
465 skolems = everythingOnTypes (<>) go where function
/dports/math/cvc4/CVC4-1.7/src/options/
H A Ddatatypes_options.toml41 help = "introduce reference skolems for shorter explanations"
/dports/math/vampire/vampire-4.5.1/Shell/
H A DNewCNF.cpp1243 Stack<Formula*> skolems; in toClauses() local
1254 skolems.push(f); in toClauses()
1265 Formula* skolem = skolems.pop(); in toClauses()
/dports/devel/hs-hls-install/haskell-language-server-1.4.0/
H A DChangeLog.md1366 - Discover skolems in the hypothesis, not just goal

12